Anthropic ha pubblicato un repository con una prova formale dell'Ultimo teorema di Fermat. Decine di agenti Claude hanno tradotto in Lean una variante dell'argomento classico di Wiles, Taylor e altri, permettendo al computer di controllare ogni passaggio logico. Secondo l'azienda il lavoro è durato undici giorni, ha generato circa 13 milioni di righe e ha usato circa 29.500 teoremi intermedi nel ramo finale.

La parola «prova» richiede cautela. Claude non ha scoperto una nuova soluzione del problema risolto negli anni Novanta. La novità è la traduzione completa e verificabile di una grande porzione di matematica moderna. Il risultato poggia su anni di lavoro delle comunità Lean e Mathlib e del progetto di Kevin Buzzard; il suo giudizio positivo è rilevante, ma una verifica indipendente più ampia è appena iniziata.

Gli agenti hanno avuto successo dopo l'adozione di Prove2Me, piattaforma che divide l'obiettivo in un grafo di teoremi minori, conserva lo stato e facilita il riuso. Il risultato misura quindi non solo il modello, ma anche orchestrazione, librerie e basi preparate dagli esseri umani. Il repository è pubblico con licenza Apache 2.0.

Se il metodo sarà generalizzabile, potrebbe trasformare articoli in forme controllabili, scoprire lacune e aiutare a revisionare la crescente matematica assistita dall'IA. Certificati formali potrebbero accompagnare risultati usati in crittografia, verifica dei chip o software critico. Non sostituirebbero comunque spiegazioni leggibili né il giudizio umano sull'adeguatezza delle ipotesi.

Per l'uso pratico bisogna ridurre l'enorme volume di codice e calcolo, riprodurre i controlli con strumenti indipendenti e dimostrare affidabilità su lavori nuovi privi di una simile infrastruttura. In uno scenario ottimistico, assistenti utili ai gruppi di formalizzazione potrebbero arrivare in 1–3 anni e allegati formali per alcuni articoli in 3–7 anni. La verifica automatica ordinaria della maggior parte della nuova matematica è più lontana e oggi non ha una data credibile.