Anthropic afirmă că AI-ul său Claude tocmai a scris cea mai lungă demonstrație matematică realizată vreodată și a folosit-o pentru a demonstra formal Marea Teoremă a lui Fermat, o problemă care i-a zăpăcit pe matematicieni timp de 358 de ani.

Claude a reușit acest lucru în 11 zile, în mare parte pe cont propriu, producând 13 milioane de linii de cod pe care un computer le poate verifica rând cu rând, în loc să se bazeze doar pe cuvântul unui matematician.

Ultima teoremă a lui Fermat spune că nu poți lua trei numere întregi pozitive, să le ridici pe fiecare la o putere mai mare decât 2, și să ai primele două adunate să dea al treilea. El a mâzgălit această afirmație pe marginea unei cărți de matematică în 1637, adăugând că avea o "dovadă cu adevărat minunată" pe care marginea era pur și simplu prea mică pentru a o cuprinde.

Apoi a murit. Matematicienii au petrecut următorii 358 de ani încercând să reconstituie ceea ce credea el că avea.

A demonstra ceva și a verifica sunt două sarcini diferite

O demonstrație matematică este un lanț de pași logici, iar dacă o verigă este ruptă, întregul colapsează. Găsirea acelei verigi rupte, îngropată undeva într-o sută de pagini de argumentație densă, le poate lua altor matematicieni ani din viață.

Formalizarea unei demonstrații înseamnă traducerea ei într-un limbaj atât de literal încât un computer poate verifica fiecare pas pe cont propriu, fără a intra în subiectivități.

Matematicienii nu au fost foarte buni la a supraveghea acest aspect de ceva timp. Un premiu german din 1908, în valoare de aproximativ 1 până la 2 milioane de dolari în banii de astăzi, oferit pentru prima demonstrație validă a teoremei, a atras 621 de trimiteri greșite doar în primul său an.

Adevărata demonstrație a apărut abia în 1995, de la matematicianul britanic Andrew Wiles, și a venit cu o întorsătură de situație. Wiles și-a anunțat soluția în cadrul a trei prelegeri în iunie 1993, doar pentru ca un recenzor să găsească o lacună în ea mai târziu.

El a petrecut aproape un an reparând-o împreună cu un fost student, Richard Taylor, aproape a renunțat și, în cele din urmă, a publicat o demonstrație corectată, de 129 de pagini, în mai 1995. Aceasta s-a bazat pe matematică care nu exista în timpul vieții lui Fermat, ceea ce este un motiv important pentru care matematicienii se îndoiesc acum că propria "dovadă minunată" a lui Fermat a funcționat vreodată.

Matematicianul Kevin Buzzard de la Imperial College London a demarat un proiect în 2024 pentru a face exact ceea ce tocmai a făcut Claude: să traducă demonstrația lui Wiles în Lean, un limbaj pe care computerele îl pot verifica. Este genul de sarcină care necesită o armată de matematicieni voluntari — propria schiță a proiectului are 86 de pagini, iar finanțarea sa este asigurată până în 2029.

Claude a finalizat totul în 11 zile.

Cum a reușit Claude de fapt

Anthropic explică într-o postare mai detaliată că Tianyi Peng, care construiește instrumente de formalizare AI cu o echipă la Columbia, a decis să vadă cât de departe ar putea ajunge Claude pe cont propriu. Zeci de agenți Claude au lucrat în paralel, scriind definiții, demonstrând rezultate mici și cumulându-le în altele mai mari, cu aproape nici o intervenție umană în afară de o ocazională sugestie precum „prioritizează următoarea teoremă”.

La început nu a mers fără probleme. Inițial, agenții pierdeau constant evidența a ceea ce demonstraseră deja și încetau să colaboreze, iar aceste începuturi false reprezintă încă aproximativ 7% din liniile demonstrației finale.

Ceea ce a rezolvat problema a fost un instrument numit Prove2Me, construit tot de echipa lui Peng, care a oferit fiecărui agent aceeași listă de sarcini în timp real, indicând ce demonstrații mai mici trebuiau încă făcute, astfel încât nimeni să nu dubleze munca sau să se abată de la sarcină. De asemenea, a organizat fișierele astfel încât Lean să poată verifica totul mai rapid și a păstrat note în engleză simplă pentru fiecare rezultat, astfel încât agenții să poată reutiliza munca celorlalți în loc să o reinventeze.

Până la finalizare, Claude demonstrase peste 30.000 de teoreme de susținere și consumase miliarde de token-uri, funcționând pe un model de cercetare pe care Anthropic spune că este aproximativ comparabil cu Claude Fable 5.1, versiunea pe care a lansat-o ulterior publicului. Demonstrația finală are 13 milioane de linii — de peste cinci ori dimensiunea Mathlib, biblioteca partajată pe care matematicienii o folosesc deja pentru acest tip de muncă.

Un roman tipic are 80.000 de cuvinte. Demonstrația lui Claude este echivalentă cu 160 de romane de argumentație pur logică.

Așadar, contează asta cu adevărat?

Buzzard — a cărui proprie versiune a acestui proiect rămâne finanțată până în 2029 — a revizuit demonstrația lui Claude și și-a dat binecuvântarea, spunând că aceasta demonstrează teorema „fără alte presupuneri în afară de axiomele matematicii”.

Acest lucru nu este același cu Claude descoperind matematică nouă, lucru pe care Anthropic l-a susținut și în cercetarea sa în criptografie la începutul acestui an. Wiles a demonstrat deja teorema lui Fermat acum trei decenii — Claude a construit doar o chitanță verificabilă de mașină pentru aceasta. Acest lucru contează deoarece matematicienii sunt din ce în ce mai copleșiți de demonstrații neverificate, inclusiv cele scrise de AI, mai rapid decât le pot verifica oamenii manual.

De asemenea, aceste tipuri de demonstrații sunt deterministe și nu sunt predispuse la erori umane, ceea ce este foarte important în matematică.

Aceasta nu este o problemă nouă. O demonstrație asistată de calculator a conjecturii lui Kepler a durat patru ani înainte ca un comitet de revizuire să se declare doar „99% sigur”, iar demonstrația conjecturii lui Poincaré de către Grigori Perelman a durat cam la fel de mult pentru a fi pe deplin înțeleasă.

Dacă nu vreți să credeți pe cuvânt pe Anthropic în legătură cu toate acestea, nu trebuie. Demonstrația completă de 13 milioane de linii se află chiar acum pe GitHub, disponibilă gratuit pentru orice matematician cu suficient timp liber pentru a o diseca, linie cu linie.