AI Research28 ott 2026

Anche Claude confuta l'ETH, da solo e in parallelo a OpenAI

Un modello di ricerca interno Claude ha trovato l'algoritmo il 16 ottobre, lo stesso giorno della prova di OpenAI, con 14M token di output e nessun input umano. I ricercatori Anthropic hanno solo aiutato a scrivere il paper "A 2^{o(n)} Time Algorithm for 3-SAT", firmato da Claude (su Hexagon dal 27 ottobre)
L'algoritmo è deterministico e conta le soluzioni di #3-SAT in tempo 2^{O(n log log n/√log n)} (per k-SAT con un fattore k²). Cade quindi anche la SETH; resta in piedi l'ipotesi Orthogonal Vectors. Le idee chiave: reti tensoriali e l'identità degli otto quadrati (1818)
Verificato in Lean 4: 1.050 moduli su Mathlib, solo i tre assiomi standard; la prova passa il kernel di Lean, leanchecker e il kernel indipendente nanoda
in attesa di revisione umana: il Lean l'hanno scritto e rivisto modelli AI e a oggi non risulta controllato da una persona. Se gli enunciati dicono davvero "l'ETH è falsa" deve giudicarlo chi li legge
Nessun uso pratico: con m = 5n clausole batte la forza bruta solo per n > 10^10.000. Però Claude ha contato oltre 800 paper con risultati che valgono solo sotto l'ETH o ipotesi più forti
Paper, Lean e istruzioni per ricontrollare sono pubblici. Secondo il README, Claude Opus 5.5 con effort alto ritrova la confutazione da un riassunto di poche righe

Fonti

AI Research28 ott 2026

Un modello di ricerca interno Claude ha trovato l'algoritmo il 16 ottobre, lo stesso giorno della prova di OpenAI, con 14M token di output e nessun input umano. I ricercatori Anthropic hanno solo aiutato a scrivere il paper "A 2^{o(n)} Time Algorithm for 3-SAT", firmato da Claude (su Hexagon dal 27 ottobre)
L'algoritmo è deterministico e conta le soluzioni di #3-SAT in tempo 2^{O(n log log n/√log n)} (per k-SAT con un fattore k²). Cade quindi anche la SETH; resta in piedi l'ipotesi Orthogonal Vectors. Le idee chiave: reti tensoriali e l'identità degli otto quadrati (1818)
Verificato in Lean 4: 1.050 moduli su Mathlib, solo i tre assiomi standard; la prova passa il kernel di Lean, leanchecker e il kernel indipendente nanoda
in attesa di revisione umana: il Lean l'hanno scritto e rivisto modelli AI e a oggi non risulta controllato da una persona. Se gli enunciati dicono davvero "l'ETH è falsa" deve giudicarlo chi li legge
Nessun uso pratico: con m = 5n clausole batte la forza bruta solo per n > 10^10.000. Però Claude ha contato oltre 800 paper con risultati che valgono solo sotto l'ETH o ipotesi più forti
Paper, Lean e istruzioni per ricontrollare sono pubblici. Secondo il README, Claude Opus 5.5 con effort alto ritrova la confutazione da un riassunto di poche righe