Repozitorijs fluid_lean GitHub parādījās 8. septembrī plkst. 4.03 pēc UTC ar vienu vienīgu komitu. Tajā ir 3748 faili ar paplašinājumu .lean un 124 412 181 baits pirmkoda. Nav ne README, ne licences faila, tikai trīs mapes: affinecore, boussinesq-blowup un euler-blowup.
Kods ir formāls pierādījums tam, ka trīsdimensiju nesaspiežamo Eilera vienādojumu atrisinājums ar gludu ārējo spēku ierobežotā laikā uzsprāgst. Autori ir Levent Alpöge un Ņujorkas universitātes matemātiķis Tristan Buckmaster. Lielāko daļu teksta uzrakstīja valodas modeļi, bet katru soli pārbaudīja Lean.
Ko tieši satur repozitorijs
Sadalījums pa mapēm izskatās šādi: affinecore 1181 fails un 20,2 MB, boussinesq-blowup 1453 faili un 35,1 MB, euler-blowup 1114 faili un 69,1 MB. Visās trīs mapēs lean-toolchain norāda vienu un to pašu versiju, leanprover/lean4:v4.32.2.
Failu nosaukumi neizskatās pēc cilvēka rakstītas bibliotēkas. Mapē AffineCore/Construction/Assembly guļ Prop71Aux.lean, Prop71BaseAux.lean, Thm72Aux.lean, Thm72oaAux.lean, Prop73Aux.lean, LipschitzClassAux.lean. Katrs no tiem ir 20 līdz 50 kilobaitus liels. Pirmajās stundās pēc publiskošanas repozitorijam bija 141 zvaigzne un 11 atzarojumi. Tā ir apgalvojumu numerācija no raksta, kas mehāniski pārlikta failu sistēmā, ar palīglemmu kaudzi zem katra numura.
Uzsprāgšana šeit nozīmē to, ka gluda sākuma stāvokļa virpuļojums ierobežotā laika sprīdī aiziet bezgalībā. Fizikā tas ir brīdis, kad vienādojums beidz aprakstīt plūsmu. Skaitliskā modelēšana šādu punktu var tikai apiet, jo režģis kļūst bezjēdzīgs, tāpēc jautājums gadu desmitiem palicis pierādījumu ziņā.
Pierādījums attiecas uz vienādojumiem ar spēka locekli. Bez tā jautājums par Eilera vienādojumu singularitāti joprojām ir atvērts, tāpat kā Navjē-Stoksa gadījums, par kuru Clay matemātikas institūts sola miljonu dolāru.
Trīs nedēļas no atrisinājuma līdz verifikācijai
Alpöge un Buckmaster pirmo uzsprāgstošo atrisinājumu ieguva 15. augustā. Lean pārbaude bija gatava 22. augustā, tātad nedēļu vēlāk. Publiskošana notika 8. septembrī, kad parādījās trīs raksti par nesaspiežamo porainās vides vienādojumu, divdimensiju Boussinesq sistēmu un Eilera vienādojumiem.
Darbā izmantoti Claude un Codex. Claude meklēja konstrukcijas galvenos elementus un atkārtoja argumentus, Codex rakstīja pamattekstu. Vēlākajās iterācijās autori piesaistīja modeļus ar apzīmējumiem 5.6 Sol un Astra.
Buckmaster par pirmajām mašīnas versijām izteicies bez aplinkiem. Pierādījums, ko modelis izspļāva, esot bijis viņa dzīvē visbriesmīgāk lasāmais. Boussinesq raksta ievadā teikts, ka pirmais modeļa uzrakstītais teksts bija sliktākais, ko autori matemātikā redzējuši. Nākamās nedēļas aizgāja ar to, lai formāli pareizo, bet nelasāmo materiālu pārrakstītu profesionālā līmenī.
Kāpēc verifikācija maina lasīšanas kārtību
Parasti matemātisku rakstu vispirms lasa recenzenti. Tas aizņem mēnešus. Šeit secība ir apgriezta. Lean kompilators jau ir pateicis, ka arguments turas kopā, tāpēc atlikušais jautājums ir tikai tas, vai formalizētais apgalvojums patiešām atbilst tam, kas rakstīts angliski.
Tā ir praktiska atbilde uz problēmu, ar kuru saskaras ikviens, kas laiž modeli pie sarežģīta uzdevuma. Modelis raksta pārliecinoši arī tad, kad kļūdās. Lean neinteresē pārliecinošs teksts, tam vajag tipu, kas saiet kopā. Šajā projektā pierādījums bija tik nelasāms, ka cilvēka recenzija praktiski nebija iespējama, tāpēc kompilators uz vairākām nedēļām palika vienīgais recenzents.
Terence Tao par darbu uzrakstīja savā blogā jau 7. septembrī, dienu pirms publiskošanas.
Ievērojams sasniegums. Nav redzams principiāls šķērslis, kas neļautu metodes attiecināt uz Navjē-Stoksa vienādojumiem, lai gan būtiskas tehniskas grūtības paliek.
Metode nav radusies tukšā vietā. Diego Córdoba un Luis Martínez-Zoroa vairāku gadu laikā izstrādāja pieeju porainās vides vienādojumam. Alpöge ar Buckmaster to pārnesa uz pārējām divām sistēmām. Porainās vides raksta līdzautors ir Matei P. Coiculescu.
Strīds par to, kas bija pirmais
Kopā ar rakstiem Buckmaster publicēja paziņojumu par divām sarunām ar OpenAI 6. septembrī. Pēc viņa stāstītā, Sébastien Bubeck teicis, ka OpenAI iekšējais modelis izveidojis aptuveni 100 lappušu garu pierādījumu Navjē-Stoksa gadījumam ar spēka locekli. Buckmaster apraksta divus piedāvājumus: publicēt vienlaikus vai uzņemties rezultāta autorību. Viņš apgalvo, ka Bubeck divreiz mudinājis no autoru saraksta izņemt Alpöge, jo tas strādā Anthropic.
Buckmaster abus piedāvājumus noraidīja. Savā paziņojumā viņš uzsver, ka OpenAI pierādījumu nav redzējis un nezina, ko modelis īsti sarakstījis. Bubeck apgalvojumus noraida kā nepatiesus un kūdošus.
Paralēli Caltech grupa, kurā strādā Ganeshram, Duruisseaux un Anandkumar, ar fizikā balstītiem neironu tīkliem meklēja pašlīdzīgus uzsprāgšanas profilus Eilera vienādojumiem bez spēka locekļa. Tao atzīmē, ka atlikums tur ir aptuveni 0,004 L bezgalības normā, taču atvasinājumu robežas, kas vajadzīgas tuvējo gludo atrisinājumu pierādīšanai, publicētas nav.
Kas paliek pārbaudāms
Repozitorijs ir bez licences, tāpēc formāli neviens to nedrīkst kopēt vai izmantot atvasinātā darbā. Būvēšanai vajadzīgs Lean 4.32.2 kopā ar Mathlib. Simts divdesmit četri megabaiti pierādījuma koda nozīmē vairāku stundu kompilāciju uz parastas darbstacijas. Kurš pirmais to izdarīs no nulles, tas arī pateiks, vai galvenā teorēma formulējumā sakrīt ar rakstos apgalvoto.
Komentāri
Šim rakstam vēl nav komentāru. Esi pirmais, kurš dalās ar savu viedokli.