Anche Anthropic dichiara falsa l'ETH: l'algoritmo per 3-SAT trovato da Claude

Il 27 ottobre 2026, poche ore dopo l'annuncio di OpenAI, anche Anthropic ha pubblicato un paper che dichiara falsa l'Exponential Time Hypothesis (ETH). Il titolo è «A 2^o(n) Time Algorithm for 3-SAT», la firma è «Claude, Anthropic»: secondo l'azienda l'algoritmo è stato trovato da un modello Claude interno di ricerca. È il secondo laboratorio in due giorni a sostenere lo stesso risultato. Ed è, come quello di OpenAI, una dichiarazione non ancora verificata dalla comunità scientifica.

Cosa ha pubblicato Anthropic#

Tre cose, tutte pubbliche:

• il paper di 49 pagine, datato 26 ottobre 2026, nella cartella eth del repository ufficiale anthropics/formal-math, aggiunta il 27 ottobre alle 04:07 ora di Roma;

• la prova formale in Lean 4, nella stessa cartella;

• il preprint su Hexagon, «Contributed by Anthropic», depositato il 27 ottobre da Jelani Nelson per conto dell'azienda.

L'abstract è netto: «We refute the Exponential Time Hypothesis (ETH) by presenting a deterministic algorithm for 3-SAT on n variables that runs in 2^o(n) time». E aggiunge che l'algoritmo risolve un problema più difficile, contare tutte le soluzioni (#3-SAT).

Cos'è l'ETH, in breve#

Il problema 3-SAT chiede se una formula logica con n variabili, scritta come insieme di clausole da tre termini, può essere resa vera. Provare tutte le combinazioni costa 2^n passi. L'ETH, proposta da Impagliazzo e Paturi, dice che non si può fare molto meglio: nel caso peggiore serve comunque un tempo esponenziale, 2^Ω(n). Il miglior algoritmo deterministico noto finora girava in circa 1,328^n.

Su questa ipotesi poggiano moltissimi risultati di complessità. Con una ricerca bibliografica fatta da Claude, scrive Anthropic, sono stati trovati più di 800 articoli che dimostrano almeno un risultato solo assumendo l'ETH o un'ipotesi che la implica.

Cosa dichiara il paper#

Il Teorema 1 descrive un algoritmo deterministico che conta le soluzioni di una formula in tempo circa 2^O(n · log log n / √log n). È meno di qualsiasi esponenziale 2^(δn), per quanto piccolo sia δ: per questo si parla di tempo subesponenziale, 2^o(n). Se il risultato regge, le conseguenze dichiarate sono molte:

• cade anche la Strong ETH (SETH), ma non l'ipotesi Orthogonal Vectors, su cui poggiano altri limiti inferiori;

• problemi come Independent Set, Clique, Vertex Cover e Dominating Set diventano risolvibili in O(2^(δn)) per ogni δ > 0;

• si ottiene un nuovo limite sui circuiti: la classe E^NP non ha circuiti booleani di dimensione lineare.

Due laboratori, stesse date#

Il dettaglio più curioso è la coincidenza. Secondo il paper, «the core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input». Lo stesso giorno, secondo OpenAI, il suo sistema scriveva la prova in linguaggio naturale della stessa tesi. Il paper di Anthropic lo riconosce: «Independently and concurrently, an internal model at OpenAI claims to have proven a similar result».

Le persone, precisa Anthropic, sono intervenute dopo: «Anthropic researchers worked with Claude to improve the presentation, resulting in this paper». Il README aggiunge un dato interessante: Claude Opus 5.5, impostato su «high effort», riesce a ricavare la versione base del risultato partendo da una descrizione condensata che il repository riporta.

Solo teoria, per ora#

Anthropic è molto chiara su un punto: «The result is purely asymptotic and says nothing about solving formulas in practice». I numeri del paper lo mostrano:

• con formule da 5n clausole, il bound batte la forza bruta solo se n supera 10^10.000;

• il bound che dipende solo da n non la batte finché n non supera 10^(10^8);

• l'approccio generale difficilmente porta guadagni sotto n = 10^7, mentre la forza bruta è già impraticabile a n = 100.

Il paper scrive anche che il risultato «does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems». Nessun solver diventa più veloce domani.

Cosa garantisce la prova in Lean#

Lean è un programma che controlla le dimostrazioni passaggio per passaggio. L'Appendice E del paper descrive la verifica: la prova usa solo i tre assiomi standard ed è accettata dal kernel di Lean, dal controllore leanchecker modulo per modulo e, tramite Comparator, da un secondo kernel scritto in modo indipendente (nanoda). Tutti i 1.050 moduli sono stati compilati da zero.

Ci sono però tre limiti, e li scrive Anthropic stessa.

• L'enunciato. Che le definizioni formali dicano davvero ciò che devono dire «no machine can check; that is for the reader».

• Chi l'ha scritta. «The Lean development was written by AI models and reviewed by other instances of the same models; at the time of writing no person is known to have checked it».

• Lo stato. Il repository è un «research artifact», non mantenuto. Il preprint non è passato da revisione paritaria.

Cosa cambia per chi lavora con l'AI#

Per un'azienda, oggi, niente di pratico: lo dice il paper. Il segnale interessante è un altro. Due laboratori diversi mostrano modelli che producono risultati controllabili da un programma, non solo testi convincenti. È un'abitudine che vale anche fuori dalla ricerca: quando usate un assistente AI per numeri, analisi o codice, chiedete qualcosa che si possa ricontrollare, come fonti, test o calcoli da rifare.

Domande frequenti#

Fonti#

• Repository anthropics/formal-math, cartella eth: paper, README e prova Lean, commit del 27/10/2026.

• Preprint su Hexagon, 2610.00577v1, «Contributed by Anthropic», 27/10/2026.

• Post di Levent Alpoge (Anthropic) su X, 27/10/2026.

• Per il confronto: repository openai/math, con il manoscritto di OpenAI sull'ETH.