Claude formalizza in Lean l’ultimo teorema di Fermat
Anthropic ha riferito il 4 settembre 2026 che Claude ha prodotto la prima dimostrazione dell’ultimo teorema di Fermat completamente verificata al computer, scrivendo circa 13 milioni di righe di Lean e dimostrando circa 29.500 teoremi intermedi in circa 11 giorni di lavoro multi-agente in gran parte autonomo sulla piattaforma Prove2Me, usando i tre assiomi standard di Lean e un enunciato allineato all’FLT di Mathlib. Il ricercatore di Anthropic Tianyi Peng ha indicato le priorità generali; Kevin Buzzard ha esaminato il risultato definendo l’autoformalizzazione straordinaria e osservando che tali tecniche potrebbero aiutare a verificare la matematica generata dall’IA e ad alleggerire la revisione tra pari. Anthropic presenta il lavoro come verifica del percorso del teorema di Wiles (via Darmon–Diamond–Taylor), non come matematica inedita come un nuovo risultato su Riemann, né come lancio di un prodotto consumer di Claude.
Tradotto con l'aiuto dell'IA.