OpenAI-jeva matematička objava od 6. oktobra pruža čitaocima javnu zbirku od 722 rukopisa, razvrstanih u 372 porodice rezultata. Jedna porodica može da obuhvati više radova, dok formalni dokaz može da se odnosi na užu tvrdnju od one u pratećem rukopisu. Praćenje rada kroz repozitorijum do konfiguracije dokaza otkriva koja je tvrdnja izabrana za proveru.

BIG CHANGE je 7. oktobra pregledao kompletan inventar datoteka repozitorijuma, katalog i odabrane artefakte dokaza. Ovo je analiza dokumentacije i statičkih artefakata: nismo kompajlirali Lean biblioteku, pokrenuli proveru dokaza niti recenzirali matematiku. OpenAI-jeva najava opisuje objavu koja se razvija i najavljuje da će uslediti dodatne formalizacije.

Velika promena

  • Šta se promenilo: Istraživači sada mogu da prate stotine rukopisa nastalih uz pomoć veštačke inteligencije od zajedničkog javnog kataloga do pratećih datoteka, a kod nekih rezultata i do formalnih iskaza i predloženih implementacija dokaza.
  • Zašto je važno: Matematičar koji odlučuje da li da upotrebi neki rezultat može da proveri iskaz izabran za proveru, njegove pretpostavke i vezu sa radom. Organizacija repozitorijuma pomaže da se utvrdi gde se završava uži formalni rezultat, a gde počinje dodatna matematička recenzija.
  • Šta treba pratiti: OpenAI planira da doda formalizacije i sačuva revizije. Te izmene su važne svakome ko citira ovaj rad ili ga nadograđuje: recenzija mora da navede verziju i teoremu koje je ispitala.

Brojati rukopise i porodice odvojeno

Naš inventar pronašao je 722 direktorijuma rukopisa neposredno u preprints/, svaki sa po jednim PDF-om, i još 10 PDF-ova u reasoning_traces/. mapa rukopisa sadrži 372 različita unosa porodica i veze ka 722 rukopisa.

Ovi brojevi opisuju različite stvari:

Artefakt

Šta čitaoci mogu da pregledaju

Porodica rezultata

Grupa srodnih radova, uključujući prateće argumente, posledice ili alternativne dokaze.

Rukopis

Pojedinačni matematički dokument sa sopstvenim izvornim datotekama i podacima za citiranje.

Sažetak obrazloženja

Skraćen prikaz obrazloženja modela za odabrani rezultat.

Lean artefakt

Formalne definicije, iskazi i predloženi dokazi, sa vezama i konfiguracijama koje određuju šta treba proveriti.

Datoteka README repozitorijuma objašnjava ove kategorije i upozorava da nivo provere nije ujednačen. Neki rezultati nemaju formalizaciju u Lean-u, a OpenAI navodi da neformalizovan rad može sadržati probleme. Sam katalog formalizacija beleži obuhvat kao „Partial progress“, a status recenzije kao unchecked. To su metapodaci o objavi, a ne ishod provere koju je pokrenuo BIG CHANGE.

Javne datoteke mogu da se čitaju bez OpenAI naloga. U najavi se navodi da je model koji ih je generisao interni i da OpenAI radi na njegovom objavljivanju. Pristup ovim dokumentima zato ne znači i pristup tom modelu.

Fiksirajte verziju pre praćenja dokaza

Ovde je korišćen snimak repozitorijuma na komitu adc7f1241b42e322a6451854ab7e4b4c146bf78a, od 6. oktobra 2026. u 21:58:50 UTC. Veze sa tim identifikatorom vode do pregledanog snimka; veze koje sadrže main prate promenljivu podrazumevanu granu. OpenAI-jev README obećava da će sačuvati ranija izdanja kada se pojave ispravke ili revizije.

Počnite od stranice pregleda, koja grupiše porodice po matematičkoj oblasti, pa pomoću mape rukopisa pronađite određeni rad. Sačuvajte naziv njegovog direktorijuma, komit repozitorijuma i priloženi bibliografski navod. Datum rukopisa može da se razlikuje od datuma objave javne zbirke.

Porodica 003 sadrži rad sa tvrdnjom o oblasti bez nula desno od 7/8, alternativni dokaz za oblast desno od 11/12 i poseban rad o Landau-Siegel nulama. Direktorijum prvog rada datiran je 30. septembra i sadrži BibTeX navod. Navođenjem konkretnog rada čuva se razlika između ovih tvrdnji.

Njegova stranica o obuhvatu u Lean-u opisuje koje iskaze formalizacija obuhvata, navodi šta isključuje i kaže da su kasnije primene iz rada izostavljene. Povezuje zasebne iskaze za proveru rezultata o zeti, Dirichlet-ovih i Hecke-ovih L-funkcija i uniformne praznine za realne nule. Provera jednog odabranog iskaza ne predstavlja automatski sve stavke na toj stranici.

Pratite izabrani iskaz do njegove konfiguracije

OpenAI-jeva uputstva za alat Comparator koriste porodicu 003 kao primer. Comparator poredi predloženi dokaz u Lean-u sa zadatim izazovom. Primer-konfiguracija u formatu JSON bira jednu teoremu: da Rimanova zeta-funkcija nema nule kada je realni deo njenog argumenta veći od 7/8.

Konfiguracija upućuje na modul izazova i zaseban modul sa rešenjem. Dozvoljava standardne aksiome propext, Quot.sound i Classical.choice, a postavlja enable_nanoda na false. Nanoda je nezavisni proverivač koji Comparator može da koristi; ova dostavljena konfiguracija ga ne uključuje.

Datoteka izazova sadrži sorry, Lean oznaku za nedovršen dokaz. Ovde ima određenu ulogu: daje iskaz sa kojim treba uporediti rešenje. Comparator-ova dokumentacija dozvoljava ovu oznaku u izazovu, ali zahteva ispravan dokaz u rešenju. Pronalaženje sorry u ovom izazovu samo po sebi ne govori ništa o tome da li zasebno rešenje prolazi proveru. Comparator-ova dokumentacija.

Za dokumentovanu lokalnu proveru potrebni su ta konfiguracija, moduli izazova i rešenja i njihove zavisnosti. Repozitorijum fiksira verziju Lean 4.34.1. Njegov Lake manifest beleži revizije zavisnosti, uključujući Mathlib na verziji d13f23b723b8a846827a245b89c10fc7d3f11612.

OpenAI zahteva comparator, landrun i lean4export u putanji za pretragu izvršnih datoteka, a zatim dokumentuje ove komande iz direktorijuma lean/:

Terminal
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

Ovo su uputstva izdavača, a ne komande koje smo pokrenuli. Uputstva ne fiksiraju verzije te tri spoljne alatke. Aktuelna Comparator dokumentacija zahteva kompatibilno okruženje lean4export, opisuje preduslove izolovanog okruženja i navodi uslove pod kojima uspešna provera potvrđuje podudaranje sa izazovom, dozvoljenu upotrebu aksioma i prihvatanje u kernel-u. Izveštaj koji može da se ponovi morao bi da zabeleži instalirane verzije alatki i stvarni izlaz, kao i komit repozitorijuma.

Datoteka README Lean biblioteke preporučuje kompajliranje manjih delova ove velike biblioteke. Takođe dokumentuje ograničenja Linux mapiranja memorije koja mogu sprečiti potpunu izgradnju. Za ovaj primer nemamo izmereno lokalno vreme izvršavanja niti trošak hardvera.

Tumačite uspešnu proveru u okviru navedenog obuhvata

Lean-ova referenca za validaciju, konsultovana u verziji 4.35.0-rc3, razlikuje prihvatanje formalnog dokaza od tumačenja značenja teoreme. Ta verzija dokumentacije odvojena je od alata fiksiranog u ovom repozitorijumu.

Uspešna osnovna provera znači da je kernel prihvatio formalni iskaz u skladu sa svojim definicijama, uvozima i aksiomima. Zavisnosti i dalje mogu sadržati nedovršene dokaze. Lean dokumentuje #print axioms za prikaz upotrebljenih aksioma, uključujući sorryAx kada u lancu zavisnosti postoji nedovršen dokaz.

Strože provere ponovo izvršavaju sačuvane dokaze ili porede rešenje sa zasebno zadatim iskazom. I dalje zavise od okruženja za proveru i od toga da li je nameravano značenje ispravno izraženo. Zato izveštaj o proveri treba da navede tačan izazov, dozvoljene aksiome i podešavanja spoljnog proverivača. Ni prihvatanje u kernel-u ni podudaranje sa izazovom ne dokazuju da je časopis prihvatio rad niti da je formalizovana svaka tvrdnja u rukopisu.

Podatak o računarskom naporu opisuje generisanje

OpenAI navodi da je prosečan rezultat zahtevao računarski napor ekvivalentan približno trima satima razmišljanja ChatGPT Pro-a. U README-u piše da je evaluacija obuhvatila oko 4.000 problema, čiji su rezultati potom grupisani i odabrani prema značaju. Navode se i izuzeci od uobičajenog postupka. To su podaci kompanije o generisanju; ne određuju cenu Lean provere za čitaoca niti ukupan iznos u dolarima. Najava objave, opis generisanja.

Za porodicu 003 ovaj pregled izdvaja konkretan iskaz o zeti, predloženo rešenje i aksiome koje proverivač dozvoljava. Takođe utvrđuje da je Nanoda isključena u datom primeru. Da li će podešena provera uspeti ostaje pitanje za pokrenut i zabeležen postupak.

Izvori i dodatna literatura

  • OpenAI-jeva najava od 6. oktobra potvrđuje datum objave, interni status modela, planirane dodatke i procenu računarskog napora. To je prikaz sopstvenog rada koji daje njegov tvorac.
  • Fiksirani repozitorijum sadrži katalog, datoteke rukopisa i konfiguracije dokaza koje smo ovde pregledali. Brojevi potiču iz kompletnog inventara i mape rukopisa; odabrane formalne datoteke pročitane su bez pokretanja. Pregledali smo i LaTeX izvor pregleda radi razumevanja organizacije.
  • Lean-ova referenca za validaciju objašnjava značenje i ograničenja provere dokaza. Koristili smo verziju 4.35.0-rc3; OpenAI projekat fiksira Lean 4.34.1.
  • Comparator dokumentacija objašnjava datoteke izazova i rešenja, uslove okruženja i uslovna obećanja. Ne navodi rezultat provere ove zbirke.
  • Recenzija Curtis Pyke-a za Kingy.ai pruža nezavisnu statičku analizu objave. Izričito navodi da nije samostalno pokretao Lean; ne smatramo je ponovljenom proverom dokaza.
  • Raniji izveštaj BIG CHANGE-a o matematici i veštačkoj inteligenciji obuhvata period od maja do septembra. Ovaj članak ispituje strukturu artefakata nove zbirke i postupak njihovog pregleda.