OpenAI-јева математичка објава од 6. октобра пружа читаоцима јавну збирку од 722 рукописа, разврстаних у 372 породице резултата. Једна породица може да обухвати више радова, док формални доказ може да се односи на ужу тврдњу од оне у пратећем рукопису. Праћење рада кроз репозиторијум до конфигурације доказа открива која је тврдња изабрана за проверу.

BIG CHANGE је 7. октобра прегледао комплетан инвентар датотека репозиторијума, каталог и одабране артефакте доказа. Ово је анализа документације и статичких артефаката: нисмо компајлирали Lean библиотеку, покренули проверу доказа нити рецензирали математику. OpenAI-јева најава описује објаву која се развија и најављује да ће уследити додатне формализације.

Велика промена

  • Шта се променило: Истраживачи сада могу да прате стотине рукописа насталих уз помоћ вештачке интелигенције од заједничког јавног каталога до пратећих датотека, а код неких резултата и до формалних исказа и предложених имплементација доказа.
  • Зашто је важно: Математичар који одлучује да ли да употреби неки резултат може да провери исказ изабран за проверу, његове претпоставке и везу са радом. Организација репозиторијума помаже да се утврди где се завршава ужи формални резултат, а где почиње додатна математичка рецензија.
  • Шта треба пратити: OpenAI планира да дода формализације и сачува ревизије. Те измене су важне свакоме ко цитира овај рад или га надограђује: рецензија мора да наведе верзију и теорему које је испитала.

Бројати рукописе и породице одвојено

Наш инвентар је пронашао 722 директоријума рукописа непосредно у preprints/, сваки са по једним PDF-ом, и још 10 PDF-ова у reasoning_traces/. мапа рукописа садржи 372 различита уноса породица и везе до 722 рукописа.

Ови бројеви описују различите ствари:

Артефакт

Шта читаоци могу да прегледају

Породица резултата

Група сродних радова, укључујући пратеће аргументе, последице или алтернативне доказе.

Рукопис

Појединачни математички документ са сопственим изворним датотекама и подацима за цитирање.

Сажетак образложења

Скраћен приказ образложења модела за одабрани резултат.

Lean артефакт

Формалне дефиниције, искази и предложени докази, са везама и конфигурацијама које одређују шта треба проверити.

Датотека README репозиторијума објашњава ове категорије и упозорава да ниво провере није уједначен. Неки резултати немају формализацију у Lean-у, а OpenAI наводи да неформализован рад може садржати проблеме. Сам каталог формализација бележи обухват као „Partial progress“, а статус рецензије као unchecked. То су метаподаци о објави, а не исход провере коју је покренуо BIG CHANGE.

Јавне датотеке могу да се читају без OpenAI налога. У најави се наводи да је модел који их је генерисао интерни и да OpenAI ради на његовом објављивању. Приступ овим документима зато не значи и приступ том моделу.

Фиксирајте верзију пре праћења доказа

Овде је коришћен снимак репозиторијума на комиту adc7f1241b42e322a6451854ab7e4b4c146bf78a, од 6. октобра 2026. у 21:58:50 UTC. Везе са тим идентификатором воде до прегледаног снимка; везе које садрже main прате променљиву подразумевану грану. OpenAI-јев README обећава да ће сачувати ранија издања када се појаве исправке или ревизије.

Почните од странице прегледа, која групише породице по математичкој области, па помоћу мапе рукописа пронађите одређени рад. Сачувајте назив његовог директоријума, комит репозиторијума и приложени библиографски навод. Датум рукописа може да се разликује од датума објаве јавне збирке.

Породица 003 садржи рад са тврдњом о области без нула десно од 7/8, алтернативни доказ за област десно од 11/12 и посебан рад о Landau-Siegel нулама. Директоријум првог рада датиран је 30. септембра и садржи BibTeX навод. Навођењем конкретног рада чува се разлика између ових тврдњи.

Његова страница о обухвату у Lean-у описује које исказе формализација обухвата, наводи шта искључује и каже да су касније примене из рада изостављене. Повезује засебне исказе за проверу резултата о зети, Dirichlet-ових и Hecke-ових L-функција и униформне празнине за реалне нуле. Провера једног одабраног исказа не представља аутоматски све ставке на тој страници.

Пратите изабрани исказ до његове конфигурације

OpenAI-јева упутства за алатку Comparator користе породицу 003 као пример. Comparator пореди предложени доказ у Lean-у са задатим изазовом. Пример-конфигурација у формату JSON бира једну теорему: да Риманова зета-функција нема нуле када је реални део њеног аргумента већи од 7/8.

Конфигурација упућује на модул изазова и засебан модул са решењем. Дозвољава стандардне аксиоме propext, Quot.sound и Classical.choice, а поставља enable_nanoda на false. Nanoda је независни проверивач који Comparator може да користи; ова достављена конфигурација га не укључује.

Датотека изазова садржи sorry, Lean ознаку за недовршен доказ. Овде има одређену улогу: даје исказ са којим треба упоредити решење. Comparator-ова документација дозвољава ову ознаку у изазову, али захтева исправан доказ у решењу. Проналазак sorry у овом изазову сам по себи не говори ништа о томе да ли засебно решење пролази проверу. Comparator-ова документација.

За документовану локалну проверу потребни су та конфигурација, модули изазова и решења и њихове зависности. Репозиторијум фиксира верзију Lean 4.34.1. Његов Lake манифест бележи ревизије зависности, укључујући Mathlib на верзији d13f23b723b8a846827a245b89c10fc7d3f11612.

OpenAI захтева comparator, landrun и lean4export у путањи за претрагу извршних датотека, а затим документује ове команде из директоријума lean/:

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

Ово су упутства издавача, а не команде које смо покренули. Упутства не фиксирају верзије те три спољне алатке. Актуелна Comparator документација захтева компатибилно окружење lean4export, описује предуслове за изоловано окружење и наводи услове под којима успешна провера потврђује поклапање са изазовом, дозвољену употребу аксиома и прихватање у kernel-у. Извештај који може да се понови морао би да забележи инсталиране верзије алатки и стварни излаз, као и комит репозиторијума.

Датотека README Lean библиотеке препоручује компајлирање мањих делова ове велике библиотеке. Такође документује ограничења Linux мапирања меморије која могу спречити потпуну изградњу. За овај пример немамо измерено локално време извршавања нити трошак хардвера.

Тумачите успешну проверу у оквиру наведеног обухвата

Lean-ова референца за валидацију, консултована у верзији 4.35.0-rc3, разликује прихватање формалног доказа од тумачења значења теореме. Та верзија документације одвојена је од алата фиксираног у овом репозиторијуму.

Успешна основна провера значи да је kernel прихватио формални исказ у складу са својим дефиницијама, увозима и аксиомима. Зависности и даље могу садржати недовршене доказе. Lean документује #print axioms за приказ употребљених аксиома, укључујући sorryAx када у ланцу зависности постоји недовршен доказ.

Строже провере поново извршавају сачуване доказе или пореде решење са засебно задатим исказом. И даље зависе од окружења за проверу и од тога да ли је намеравано значење исправно изражено. Зато извештај о провери треба да наведе тачан изазов, дозвољене аксиоме и подешавања спољног проверивача. Ни прихватање у kernel-у ни подударање са изазовом не доказују да је часопис прихватио рад нити да је формализована свака тврдња у рукопису.

Податак о рачунарском напору описује генерисање

OpenAI наводи да је просечан резултат захтевао рачунарски напор еквивалентан приближно трима сатима размишљања ChatGPT Pro-а. У README-у пише да је евалуација обухватила око 4.000 проблема, чији су резултати потом груписани и одабрани према значају. Наводе се и изузеци од уобичајеног поступка. То су подаци компаније о генерисању; не одређују цену Lean провере за читаоца нити укупан износ у доларима. Најава објаве, опис генерисања.

За породицу 003 овај преглед издваја конкретан исказ о зети, предложено решење и аксиоме које проверивач дозвољава. Такође утврђује да је Nanoda искључена у датом примеру. Да ли ће подешена провера успети остаје питање за покренути и забележени поступак.

Извори и додатна литература

  • OpenAI-јева најава од 6. октобра потврђује датум објаве, интерни статус модела, планиране додатке и процену рачунарског напора. То је приказ сопственог рада који даје његов творац.
  • Фиксирани репозиторијум садржи каталог, датотеке рукописа и конфигурације доказа које смо овде прегледали. Бројеви потичу из комплетног инвентара и мапе рукописа; одабране формалне датотеке прочитане су без покретања. Прегледали смо и LaTeX извор прегледа ради разумевања организације.
  • Lean-ова референца за валидацију објашњава значење и ограничења провере доказа. Користили смо верзију 4.35.0-rc3; OpenAI пројекат фиксира Lean 4.34.1.
  • Comparator документација објашњава датотеке изазова и решења, услове окружења и условна обећања. Не наводи резултат провере ове збирке.
  • Рецензија Curtis Pyke-а за Kingy.ai пружа независну статичку анализу објаве. Изричито наводи да није самостално покретао Lean; не сматрамо је поновљеном провером доказа.
  • Ранији извештај BIG CHANGE-а о математици и вештачкој интелигенцији обухвата период од маја до септембра. Овај чланак испитује структуру артефаката нове збирке и поступак њиховог прегледа.