Lean Jaċċetta l-Prova ta’ Fermat ta’ Claude

Lean, is-software għall-verifika tal-provi li jużaw il-matematiċi madwar id-dinja, aċċetta verżjoni formali sħiħa tal-Aħħar Teorema ta’ Fermat. Il-formalizzazzjoni, prodotta mis-sistema Claude ta’ Anthropic u ppubblikata bħala repożitorju miftuħ, ma fiha ebda pass proviżorju mhux solvut, ebda assjoma addizzjonali u ebda soluzzjoni komputazzjonali mqassra lil hinn mill-pedamenti standard ta’ Lean (repożitorju). Kevin Buzzard, il-matematiku tal-Imperial College London li kien qed imexxi l-isforz tiegħu stess ta’ formalizzazzjoni, ikkompila l-proġett b’mod indipendenti u kkonferma li għadda mill-verifika, filwaqt li sejjaħlu “kisba straordinarja fl-awtoformalizzazzjoni” (Buzzard).

Il-matematika nnifisha kienet ilha li ġiet solvuta. Andrew Wiles ipprova t-teorema fl-1995, u ebda matematiku serju ma kellu dubju dwar ir-riżultat. Dak li kien għadu mhux lest kien il-kitba mill-ġdid ta’ dik il-prova bħala struzzjonijiet għal sistema ta’ verifika litterali, billi tingħata kull definizzjoni u kull pass intermedju li l-awtur oriġinali seta’ jħalli impliċitu. Anthropic tgħid li għexieren ta’ aġenti tal-IA lestew din it-traduzzjoni fi ħdax-il jum matul Awwissu, billi ħadmu b’mod parallel permezz ta’ pjattaforma msejħa Prove2Me (Anthropic).

Madankollu, din l-iskeda ta’ żmien tiddeskrivi proċess li persuni minn barra ma jistgħux jirriproduċu. Il-mudell intern, l-infrastruttura ta’ orkestrazzjoni, id-deċiżjonijiet tal-operaturi u n-nefqa komputazzjonali mhumiex parti mir-rilaxx pubbliku. Dak li jista’ jiġi riprodott huwa l-prodott finali: kull min għandu hardware b’saħħtu biżżejjed jista’ jerġa’ jikkompila l-proġett ta’ Lean u jikkonferma li l-prova tgħaddi mill-verifika. Sistema ta’ verifika separata miktuba f’Rust minn Anthropic ivverifikat l-istess prodott formali, u kkonfermat li l-1,052,234 dikjarazzjoni kollha huma konsistenti (rapport tekniku). Din hija t-tieni verifika tal-istess test, mhux rikostruzzjoni indipendenti tal-kampanja ta’ ħdax-il jum.

Kif ħadmu l-aġenti

Il-formalizzazzjoni ta’ prova tfisser li l-argument ta’ matematiku jinkiteb mill-ġdid sabiex programm mingħajr intuwizzjoni matematika jkun jista’ jikkonferma kull pass loġiku. It-teorema nnifisha tidher sempliċi b’mod qarrieqi: għal kwalunkwe esponent sħiħ ta’ tlieta jew aktar, ma jeżistux tliet numri sħaħ pożittivi li jissodisfaw aⁿ + bⁿ = cⁿ. Madankollu, il-prova tgħaddi minn saffi profondi tat-teorija tan-numri mifruxa fuq mijiet ta’ paġni.

Claude ma skopriex matematika ġdida. Huwa fformalizza s-sensiela stabbilita ta’ riżultati li twassal għall-prova ta’ Wiles, billi segwa espożizzjoni tal-matematiċi Henri Darmon, Fred Diamond u Richard Taylor (Anthropic, rapport tekniku). L-għarfien kreattiv kien ta’ Wiles u ta’ dawk li ġew qablu. Il-kontribut ta’ Claude kien li jittraduċi dak l-għarfien f’madwar 10.5 miljun linja ta’ kodiċi li jista’ jiġi vverifikat minn magna (rapport tekniku).

Il-pjattaforma Prove2Me, iddisinjata mir-riċerkatur ta’ Anthropic Tianyi Peng u minn kollaboraturi fl-Università ta’ Columbia, qasmet il-prova fi graff ta’ dipendenzi magħmul minn madwar 29,511-il stqarrija awtonoma (rapport tekniku). L-aġenti għażlu l-istqarrijiet li kienu lesti biex jinħadmu, kitbu provi tagħhom f’Lean u vverifikaw l-istqarrijiet proposti minn xulxin, filwaqt li ħadmu b’mod parallel. Il-kampanja kkonsmat madwar sitt biljun token ta’ output minn mudell intern ta’ riċerka (rapport tekniku).

Skont Anthropic, l-operaturi umani ma kitbu ebda kodiċi f’Lean matul il-proċess, għalkemm għażlu t-teorema, ipprovdew ir-rotta magħrufa għall-prova, iddisinjaw l-infrastruttura tal-aġenti u kultant aġġustaw il-prijoritajiet (Anthropic). It-traskrizzjoni sħiħa tal-ħidma tal-operaturi u l-ispejjeż komputazzjonali ma ġewx żvelati.

Mibni fuq snin ta’ ħidma preparatorja mill-bnedmin

Ir-riżultat kien jiddependi fuq Mathlib, il-librerija kbira ta’ matematika formalizzata miżmuma mill-komunità, u bbenefika direttament minn żewġ proġetti preċedenti. It-tim ta’ Buzzard fl-Imperial kien ilu mill-aħħar tal-2023 jibni formalizzazzjoni tal-Aħħar Teorema ta’ Fermat f’Lean, iffinanzjata minn għotja ta’ £1 miljun mill-EPSRC maħsuba li tibqa’ għaddejja sal-2029 (għotja tal-EPSRC). Proġett separat tal-komunità kien diġà fformalizza t-teorema għal parti mill-każijiet. Il-fajl ta’ attribuzzjoni ta’ Anthropic jidentifika 106 fajls li fihom materjal meħud jew adattat minn dawn l-isforzi (attribuzzjoni).

L-eżekuzzjoni parallela tagħmel il-ħdax-il jum kalendarju inkomparabbli mas-sigħat ta’ xogħol uman investiti mit-tim ta’ Buzzard, li kien ilu għaddej għal madwar 22 xahar ta’ finanzjament meta bdiet il-kampanja ta’ Claude (għotja tal-EPSRC). Anthropic la żvelat is-sigħat ta’ użu tal-GPUs u lanqas l-ispejjeż tal-enerġija.

Qabel dan ir-rilaxx, l-Aħħar Teorema ta’ Fermat kienet l-aħħar punt li kien għad fadal fil-lista ta’ Freek Wiedijk ta’ 100 teorema importanti li kienu qed jistennew formalizzazzjoni, punt ta’ riferiment li ilu jkejjel il-progress għal għoxrin sena (Buzzard).

L-aktar test b’saħħtu dwar jekk dan jistax jiġi ġeneralizzat se jkun il-formalizzazzjoni ta’ matematika reċenti u inqas dokumentata, fejn ma jeżistux pjan dettaljat, libreriji maturi jew xogħol formali preċedenti. Din il-ħidma ttestjat teorema magħrufa sew b’infrastruttura sostanzjali diġà fis-seħħ. Hija turi li l-aġenti tal-IA, meta jingħataw rotta magħrufa għall-prova u xogħol formali preċedenti, jistgħu jipproduċu formalizzazzjoni sħiħa li Lean jaċċetta u li persuni minn barra jistgħu jerġgħu jivverifikaw. Il-kampanja tal-ġenerazzjoni nnifisha tibqa’ impossibbli li tiġi riprodotta mill-materjal ippubblikat.