Lean validează demonstrația Fermat a Claude

Lean, programul de verificare a demonstrațiilor folosit de matematicieni din întreaga lume, a validat o versiune formală completă a ultimei teoreme a lui Fermat. Formalizarea, realizată de sistemul Claude al Anthropic și publicată într-un registru deschis, nu conține etape provizorii nerezolvate, axiome suplimentare sau scurtături de calcul în afara fundamentelor standard ale Lean (repository). Kevin Buzzard, matematician la Imperial College London și coordonatorul unui proiect propriu de formalizare, a compilat independent codul și a confirmat că verificarea reușește, descriind rezultatul drept „o realizare extraordinară de autoformalizare” (Buzzard).

Problema matematică fusese rezolvată de mult: Andrew Wiles a demonstrat teorema în 1995, iar rezultatul nu era contestat de matematicienii reputați. Lipsea însă transcrierea demonstrației sub forma unor instrucțiuni pentru un verificator literal, căruia trebuie să-i fie furnizate toate definițiile și etapele intermediare pe care autorul le poate lăsa subînțelese. Potrivit Anthropic, zeci de agenți AI au încheiat această transcriere în 11 zile, în august, lucrând în paralel printr-o platformă numită Prove2Me (Anthropic).

Durata anunțată descrie însă un proces pe care cercetătorii din afara companiei nu îl pot reproduce. Modelul intern, infrastructura de coordonare, deciziile operatorilor și resursele de calcul consumate nu fac parte din materialele publicate. Poate fi reprodus doar rezultatul final: orice persoană care dispune de suficientă putere de calcul poate recompila proiectul Lean și poate confirma validitatea demonstrației. Un verificator separat, scris în Rust de Anthropic, a analizat același artefact formal și a confirmat coerența tuturor celor 1.052.234 de declarații (technical report). Este o a doua verificare a aceluiași text, nu o reconstrucție independentă a procesului desfășurat în 11 zile.

Cum au lucrat agenții

Formalizarea unei demonstrații presupune rescrierea argumentului matematic într-o formă în care un program lipsit de intuiție matematică să poată verifica fiecare pas logic. Enunțul teoremei este simplu: pentru orice exponent număr întreg mai mare sau egal cu trei, nu există trei numere întregi pozitive care să satisfacă ecuația aⁿ + bⁿ = cⁿ. Demonstrația parcurge însă, de-a lungul a sute de pagini, domenii avansate ale teoriei numerelor.

Claude nu a descoperit matematică nouă, ci a formalizat succesiunea cunoscută de rezultate care conduce la demonstrația lui Wiles, urmând o expunere semnată de matematicienii Henri Darmon, Fred Diamond și Richard Taylor (Anthropic, technical report). Ideile originale le aparțin lui Wiles și predecesorilor săi. Contribuția sistemului Claude a constat în transcrierea lor în aproximativ 10,5 milioane de linii de cod verificabil automat (technical report).

Platforma Prove2Me, concepută de cercetătorul Anthropic Tianyi Peng împreună cu colaboratori de la Columbia University, a împărțit demonstrația într-un graf de dependențe format din aproximativ 29.511 afirmații autonome (technical report). Agenții preluau afirmațiile pentru care premisele erau deja disponibile, scriau demonstrațiile în Lean și verificau formulările propuse de ceilalți, astfel încât mai multe componente să poată fi dezvoltate simultan. Întregul proces a consumat aproximativ șase miliarde de tokenuri de ieșire generate de un model intern de cercetare (technical report).

Potrivit Anthropic, operatorii umani nu au scris cod Lean în timpul rulării, dar au ales teorema și traseul cunoscut al demonstrației, au proiectat infrastructura agenților și au ajustat ocazional prioritățile (Anthropic). Compania nu a publicat transcrierea integrală a intervențiilor operatorilor și nici costurile de calcul.

Rezultatul se sprijină pe ani de muncă umană

Formalizarea s-a bazat pe Mathlib, vasta bibliotecă de matematică formalizată întreținută de comunitate, și a folosit direct două proiecte anterioare. Echipa lui Buzzard de la Imperial lucra din a doua parte a anului 2023 la propria formalizare în Lean a ultimei teoreme a lui Fermat, printr-un proiect finanțat până în 2029 cu un grant EPSRC de 1 milion de lire sterline (EPSRC award). Un alt proiect al comunității formalizase deja teorema pentru o parte dintre cazuri. Fișierul Anthropic privind atribuirea contribuțiilor identifică 106 fișiere care includ materiale preluate sau adaptate din aceste inițiative (attribution).

Execuția în paralel face ca cele 11 zile calendaristice să nu poată fi comparate direct cu numărul de ore de muncă investite de echipa lui Buzzard, al cărei proiect acumulase aproximativ 22 de luni de finanțare când a început campania Claude (EPSRC award). Anthropic nu a comunicat nici numărul de ore de funcționare a procesoarelor grafice, nici consumul de energie.

Înaintea acestei publicări, ultima teoremă a lui Fermat era singura problemă rămasă pe lista întocmită de Freek Wiedijk cu 100 de teoreme importante care așteptau să fie formalizate, un reper folosit de două decenii pentru măsurarea progreselor din domeniu (Buzzard).

Capacitatea metodei de a se generaliza va fi testată mai convingător prin formalizarea unor rezultate matematice recente și mai slab documentate, pentru care nu există un traseu detaliat, biblioteci mature sau proiecte formale anterioare. În acest caz, agenții au lucrat asupra unei teoreme celebre, susținuți de o infrastructură deja consistentă. Rezultatul arată că agenții AI pot produce o formalizare completă, acceptată de Lean și verificabilă de terți, atunci când primesc o demonstrație cunoscută și se pot baza pe muncă formală preexistentă. Procesul de generare nu poate fi însă reprodus din materialele publicate.