Fermat's Theorem verificato in Lean 4

Lo speciale martedì di questa rubrica riguarda un evento che appartiene tanto alla matematica quanto all'ingegneria del software: la formalizzazione completa del Fermat's Last Theorem in Lean 4. Il repository pubblicato da Anthropic contiene una prova machine-checked, costruita su Mathlib, con toolchain Lean 4.33.1 e Mathlib v4.33.0 pinnata tramite commit nel lakefile.lean, come documentato nel repository ufficiale^[1].

Cosa è cambiato tecnicamente

L'argomento formalizzato ricalca la traiettoria classica: Frey, Serre, Ribet, Wiles e Taylor-Wiles. Il file PROOF-PATH.md elenca ogni passaggio insieme al teorema Lean corrispondente, mentre la cartella html/ espone l'intera dimostrazione come pagine web navigabili offline.

Il teorema centrale, dichiarato in Theorems/Thm_fermat_last_theorem.lean, afferma che per ogni n naturale maggiore o uguale a 3 e per ogni terna di interi positivi a, b, c, vale a^n + b^n ≠ c^n. La costruzione include 60.475 moduli, tutti compilati e controllati dal kernel Lean durante una build eseguita da zero, secondo quanto riportato nel repository^[1].

Il meccanismo della doppia verifica

La build principale utilizza Lean 4.33.1, versione che integra le correzioni di solidità del kernel introdotte nel 2026. Mathlib viene ricompilato interamente da sorgente, eliminando qualsiasi dipendenza da artefatti pre-costruiti che potrebbero introdurre discrepanze silenziose. Questo elimina il rischio di ereditare bug di compilazione da versioni precedenti della libreria matematica, un problema ricorrente nei toolchain che riutilizzano cache condivise tra progetti.

Il file FinalCheck.lean impone un vincolo preciso: la build fallisce a meno che la prova poggi esattamente sui tre assiomi standard di Lean, propext, Classical.choice e Quot.sound. Zero istanze di sorry, zero assiomi aggiunti, zero uso di native_decide.

Un secondo strato di controllo arriva dal comparator leanprover/comparator v4.33.0, che confronta la build contro verification/comparator/Challenge.lean. Il verdetto riportato, "Your solution is okay!", conferma identità tra l'enunciato provato e la sfida dichiarata in Mathlib puro.

Il kernel indipendente come confine di fiducia

Il terzo livello arriva da nanoda 0.4.13, kernel Lean scritto in Rust, indipendente dall'implementazione ufficiale. Ha accettato l'export dello stesso ambiente prodotto dalla build principale.

Questo doppio controllo, kernel ufficiale più kernel alternativo, riproduce esattamente la logica del circuito di validazione indipendente che questa rubrica raccomanda per qualsiasi pipeline dove l'output di un componente diventa input del successivo. La differenza qui è che il dominio è la matematica formale, dove l'ambiguità semantica risulta assente per costruzione.

La root condition che lega matematica formale e sistemi multi-agente

La condizione strutturale comune tra questa verifica e i sistemi multi-agente aziendali è la stessa: un output critico va confermato da un percorso di validazione indipendente prima di venire considerato affidabile. La differenza è che qui esiste un kernel formale capace di eseguire quella conferma in modo deterministico.

Nei sistemi di produzione basati su modelli linguistici, quel kernel deterministico manca. L'assenza di un arbitro formale costringe i team a costruire circuit breaker espliciti, altrimenti l'errore di un agente si propaga privo di freni lungo l'intera pipeline, esattamente il meccanismo documentato negli studi su hallucination cascade.

Il rischio di trasporre il modello ad altri domini

Il rischio principale non riguarda la correttezza della prova, confermata da tre livelli di controllo indipendenti. Riguarda invece la tentazione di generalizzare il metodo a domini dove la formalizzazione completa risulta impraticabile, come la maggior parte dei processi decisionali aziendali basati su linguaggio naturale.

La matematica formale possiede una proprietà che nessun documento contrattuale o pipeline di retrieval possiede: un enunciato dimostrabile ha esattamente un valore di verità, verificabile meccanicamente. Un documento recuperato da un sistema RAG, al contrario, porta ambiguità semantica intrinseca e può contenere istruzioni malevole travestite da contenuto legittimo. Trattare l'uno come modello dell'altro produce un errore di procurement: si acquista fiducia formale per problemi che restano probabilistici.

Tre domande per i team enterprise AI

Prima di trattare questo risultato come precedente riutilizzabile, ogni team tecnico dovrebbe rispondere a tre domande operative:

1. Quale parte della pipeline aziendale dispone oggi di un equivalente del kernel indipendente, capace di confermare un output prima che diventi input a valle?
2. Quali assiomi impliciti, dipendenze, versioni, librerie pinnate, restano documentati e quali vengono assunti tacitamente?
3. Chi, nel team, ha l'autorità di bloccare una build o una release qualora il controllo indipendente riporti un esito discordante?

Decisioni per il prossimo ciclo di pianificazione

CTO e Chief Digital Officer dovrebbero rivalutare gli stack di verifica formale come categoria di investimento a sé, distinta dal generico tooling AI. Head of Engineering dovrebbero considerare l'adozione di pratiche di doppio-kernel, o comunque di validazione incrociata, per pipeline critiche dove l'errore ha costo elevato.

CFO dovrebbero leggere questo risultato come segnale che l'investimento in formal methods, storicamente considerato accademico, produce ora artefatti verificabili con costo di audit contenuto. Il Technology Procurement Committee dovrebbe rinegoziare i contratti con i vendor di tooling di verifica, chiedendo evidenza documentata di controllo indipendente equivalente a quello qui descritto.

I limiti tecnici da non ignorare

Il repository dichiara esplicitamente il proprio status: "Research artifact. Not maintained and not accepting contributions", come riportato nel repository^[1]. Questo colloca il progetto in categoria distinta da production-ready: disponibile per ispezione, esclusivamente in forma di riferimento, privo di canale di manutenzione continua.

La pagina di ricerca pubblicata da Anthropic, dedicata alla formalizzazione, inquadra l'esercizio come dimostrazione di capacità dei modelli attuali su compiti di ragionamento matematico assistito, disponibile su anthropic.com^[2]. Il divario tra "disponibile per lettura" e "pronto per l'integrazione in workflow di produzione" resta il punto che ogni comitato di procurement deve tenere fermo prima di replicare l'iniziativa su domini aziendali meno formalizzabili della teoria dei numeri.