6 ऑक्टोबरच्या OpenAI गणित प्रकाशनाने 372 निकाल गटांमध्ये मांडलेली 722 हस्तलिखितांची सार्वजनिक मालिका उपलब्ध केली. एका गटात अनेक लेख असू शकतात; औपचारिक पुरावा संबंधित हस्तलिखितापेक्षा मर्यादित विधान व्यापू शकतो. रिपॉझिटरीतील लेखाचा त्याच्या पुरावा रचनेपर्यंत मागोवा घेतल्यास तपासणीसाठी निवडलेला दावा दिसतो.

7 ऑक्टोबरला BIG CHANGE ने रिपॉझिटरीची संपूर्ण फाइल यादी, सूची आणि निवडक पुरावा कलाकृती तपासल्या. हे दस्तऐवजी आणि स्थिर फाइल विश्लेषण आहे; आम्ही Lean लायब्ररी संकलित केली नाही, पुरावा तपासक चालवला नाही किंवा गणिताचे परीक्षण केले नाही. OpenAI ची घोषणा सतत विकसित होणारे प्रकाशन वर्णन करते आणि आणखी औपचारीकरणे येतील असे सांगते.

मोठा बदल

  • काय बदलले:संशोधक आता शेकडो AI-निर्मित हस्तलिखितांचा सामायिक सार्वजनिक सूचीमधून सहाय्यक फाइलांपर्यंत आणि काही निकालांसाठी औपचारिक विधाने व प्रस्तावित पुरावा अंमलबजावण्यांपर्यंत मागोवा घेऊ शकतात.
  • हे का महत्त्वाचे:निकाल वापरायचा का हे ठरवणारा गणितज्ञ तपासणीसाठी निवडलेले विधान, त्याची गृहीतके आणि लेखाशी असलेले नाते पाहू शकतो. रिपॉझिटरीची रचना मर्यादित औपचारिक निकाल कुठे संपतो आणि पुढील गणितीय परीक्षण कुठे सुरू होते हे दाखवते.
  • कशाकडे लक्ष द्यावे:OpenAI औपचारीकरणे जोडण्याची आणि पुनरावृत्त्या जतन करण्याची योजना आखते. या कामाचा संदर्भ देणाऱ्यांसाठी किंवा त्यावर आधारित काम करणाऱ्यांसाठी हे बदल महत्त्वाचे आहेत: परीक्षणाने तपासलेली आवृत्ती आणि प्रमेय नमूद करावे.

हस्तलिखिते आणि गट वेगवेगळे मोजा

आमच्या यादीत preprints/ अंतर्गत थेट 722 हस्तलिखित संचिका आढळल्या; प्रत्येकात PDF आहे. reasoning_traces/ अंतर्गत आणखी 10 PDF आहेत. हस्तलिखित नकाशा 372 स्वतंत्र गट नोंदी आणि 722 हस्तलिखित दुवे दाखवतो.

हे आकडे वेगवेगळ्या गोष्टी दर्शवतात:

कलाकृती

वाचक काय तपासू शकतात

निकाल गट

संबंधित लेखांचा समूह, ज्यात पूरक युक्तिवाद, निष्पत्ती किंवा पर्यायी पुरावे असू शकतात.

हस्तलिखित

स्वतःच्या स्रोत फाइल्स आणि उद्धरण माहितीसह स्वतंत्र गणितीय दस्तऐवज.

युक्तिवादाचा सारांश

निवडलेल्या निकालासाठी मॉडेलच्या युक्तिवादाचे संक्षिप्त वर्णन.

Lean कलाकृती

औपचारिक व्याख्या, विधाने व प्रस्तावित पुरावे; काय तपासायचे हे दाखवणारे दुवे आणि रचना.

रिपॉझिटरीची README या श्रेणी स्पष्ट करते आणि सत्यापनाची पातळी समान नसल्याचा इशारा देते. काही निकालांना Lean औपचारीकरण नाही; औपचारिक न केलेल्या कामात समस्या असू शकतात असे OpenAI म्हणते. औपचारीकरण सूची व्याप्ती "Partial progress" आणि परीक्षण स्थिती unchecked अशी नोंदवते. हे प्रकाशन metadata आहे, BIG CHANGE ने चालवलेल्या तपासकाचा निकाल नाही.

OpenAI खात्याशिवाय सार्वजनिक फाइल्स वाचता येतात. घोषणा निर्मिती करणारे मॉडेल अंतर्गत असल्याचे आणि ते प्रसिद्ध करण्यासाठी OpenAI काम करत असल्याचे सांगते. त्यामुळे दस्तऐवजांचा प्रवेश मॉडेलचा प्रवेश सिद्ध करत नाही.

पुराव्याचा मागोवा घेण्यापूर्वी आवृत्ती निश्चित करा

येथे वापरलेला रिपॉझिटरी snapshot commit adc7f1241b42e322a6451854ab7e4b4c146bf78a आहे; तारीख 6 ऑक्टोबर 2026, 21:58:50 UTC. हा ओळख क्रमांक असलेले दुवे तपासलेला snapshot जतन करतात; main असलेले दुवे बदलणाऱ्या default branchकडे जातात. दुरुस्ती किंवा पुनरावृत्ती आल्यास जुनी प्रकाशने जतन करण्याचे OpenAI README सांगते.

सुरुवात आढाव्यापासून करा; तो गणितीय विषयांनुसार गट मांडतो. मग विशिष्ट लेख शोधण्यासाठी हस्तलिखित नकाशा वापरा. संचिकेचे नाव, रिपॉझिटरी commit आणि लेखाने दिलेले उद्धरण जतन करा. हस्तलिखिताची तारीख आणि सार्वजनिक संग्रहाची प्रकाशन तारीख वेगळी असू शकते.

गट 003 मधील एका लेखात 7/8 च्या उजवीकडील शून्यरहित क्षेत्राचा दावा आहे; 11/12 च्या उजवीकडील क्षेत्रासाठी पर्यायी पुरावा आहे; आणि Landau–Siegel शून्यांवरील स्वतंत्र लेख आहे. पहिल्या लेखाची संचिका 30 सप्टेंबरची तारीख दाखवते आणि BibTeX उद्धरण देते. विशिष्ट लेख नोंदवल्याने हे दावे वेगळे राहतात.

त्याचे Lean व्याप्ती पृष्ठ औपचारीकरण कोणती विधाने व्यापते, काय वगळते आणि लेखातील पुढील अनुप्रयोग का वगळले आहेत हे सांगते. zeta निकाल, Dirichlet आणि Hecke L-functions आणि वास्तविक शून्यांतील एकसमान अंतर यांसाठी ते स्वतंत्र तपासणी विधानांशी दुवे देते. एका निवडलेल्या विधानाची तपासणी त्या पृष्ठावरील प्रत्येक गोष्ट आपोआप तपासत नाही.

निवडलेल्या विधानाचा त्याच्या रचनेपर्यंत मागोवा घ्या

OpenAI च्या Comparator सूचना गट 003 उदाहरण म्हणून वापरतात. प्रस्तावित Lean पुराव्याची ठराविक challengeशी तुलना करणारे साधन म्हणजे Comparator. उदाहरणाची JSON रचना एक प्रमेय निवडते: argumentचा वास्तविक भाग 7/8 पेक्षा मोठा असल्यास Riemann zeta function शून्यरहित असणे.

रचना challenge module आणि स्वतंत्र solution module दाखवते. ती मानक axioms propext , Quot.sound आणि Classical.choice परवानगी देते आणि enable_nanoda चे मूल्य false ठेवते. Nanoda हा स्वतंत्र तपासक असून Comparator तो वापरू शकतो; दिलेली रचना त्याला सक्रिय करत नाही.

ही challenge फाइल मध्ये sorry आहे; अपूर्ण पुराव्यासाठीचा Lean placeholder. येथे त्याचे विशिष्ट काम म्हणजे जुळवायचे विधान पुरवणे. Comparator दस्तऐवज challengeमध्ये placeholderला परवानगी देते आणि solutionमध्ये योग्य पुरावा मागते. केवळ challengeमध्ये sorry आढळल्याने वेगळे solution पास होईल की नाही हे समजत नाही. Comparator दस्तऐवज.

दस्तऐवजीकृत स्थानिक तपासणीसाठी ही रचना, तिचे challenge व solution modules आणि त्यांची dependencies आवश्यक आहेत. रिपॉझिटरी Lean 4.34.1pin करते. त्याचा Lake manifest dependenciesच्या आवृत्त्या नोंदवतो; त्यात Mathlib ची आवृत्ती d13f23b723b8a846827a245b89c10fc7d3f11612 आहे.

OpenAI म्हणते की comparator , landrun आणि lean4export executable search pathमध्ये असावेत; त्यानंतर lean/ संचिकेतून या commands चालवण्याचे निर्देश देते:

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

ही प्रकाशकाची मार्गदर्शक माहिती आहे; आम्ही चालवलेले commands नाहीत. ती तीन बाह्य साधनांच्या आवृत्त्या pin करत नाही. Comparatorची सध्याची कागदपत्रे सुसंगत lean4export आवृत्ती मागतात; sandbox अटी आणि challengeशी जुळणे, परवानगीचे axioms वापरणे, kernelने स्वीकारणे यशस्वी कधी ठरते ते स्पष्ट करतात. पुनरुत्पादनीय अहवालात रिपॉझिटरी commitसह स्थापित साधनांच्या आवृत्त्या आणि प्रत्यक्ष output नोंदवावा.

या मोठ्या लायब्ररीचे लहान भाग संकलित करण्याची शिफारस Lean लायब्ररीची README करते. Linux memory-mapping मर्यादा पूर्ण build रोखू शकतात असेही त्यात नमूद आहे. या उदाहरणाचा स्थानिक runtime किंवा hardware खर्च आम्ही मोजला नाही.

यशस्वी तपासणी तिच्या घोषित व्याप्तीत समजून घ्या

तपासणीच्या वेळी आवृत्ती 4.35.0-rc3 असलेला Lean चा validation reference, औपचारिक पुरावा स्वीकारणे आणि प्रमेयाचा अर्थ लावणे यात फरक करतो. दस्तऐवजाची ही आवृत्ती रिपॉझिटरीत pin केलेल्या toolchainपेक्षा वेगळी आहे.

मूलभूत तपासणी यशस्वी झाली म्हणजे kernelने व्याख्या, imports आणि axiomsच्या अंतर्गत औपचारिक विधान स्वीकारले. Dependenciesमध्ये अपूर्ण पुरावे उरू शकतात. वापरलेले axioms दाखवणाऱ्या Lean #print axioms चे वर्णन केले आहे; dependency chainमधील अपूर्ण पुराव्यासाठी sorryAx वापरले जाऊ शकते.

अधिक कठोर तपासण्या जतन केलेले पुरावे पुन्हा चालवतात किंवा solutionची स्वतंत्रपणे निश्चित केलेल्या विधानाशी तुलना करतात. तरीही त्या तपासणीचे वातावरण आणि अपेक्षित अर्थ योग्य मांडला आहे का यावर अवलंबून असतात. म्हणून अचूक challenge, अनुमत axioms आणि बाह्य checker settings verification reportमध्ये नमूद करा. Kernelची स्वीकृती किंवा challengeशी जुळणे हे जर्नलची स्वीकृती किंवा हस्तलिखितातील प्रत्येक दावा औपचारिक केला असल्याचे सिद्ध करत नाही.

compute आकडा निर्मिती दर्शवतो

OpenAIच्या मते, प्रत्येक निकालासाठी सरासरी ChatGPT Proमध्ये सुमारे तीन तास विचार करण्याइतका compute वापरला. READMEनुसार evaluationमध्ये सुमारे 4,000 समस्या विचारल्या, outputs गटबद्ध केले आणि महत्त्वाचे निवडले. नेहमीच्या प्रक्रियेतील अपवादही नोंदवले आहेत. हे कंपनीचे निर्मितीविषयक आकडे आहेत; वाचकाच्या Lean तपासणीची किंमत किंवा एकूण डॉलर बिल ते सांगत नाहीत. प्रकाशन घोषणा, निर्मितीचे वर्णन.

गट 003साठी या परीक्षणात विशिष्ट zeta विधान, प्रस्तावित solution आणि checkerने परवानगी दिलेली axioms ओळखली आहेत. दिलेल्या उदाहरणात Nanoda बंद असल्याचेही स्पष्ट होते. ही रचना तपासणीत यशस्वी होते की नाही हे नोंदवलेल्या प्रत्यक्ष चाचणीतूनच कळेल.

स्रोत आणि पुढील वाचन

  • 6 ऑक्टोबरची OpenAI घोषणाप्रकाशन तारीख, मॉडेलची अंतर्गत स्थिती, नियोजित भर आणि कंपनीचा compute अंदाज याची पुष्टी करते. हे विकासकाने स्वतःच्या कामाबद्दल दिलेले वर्णन आहे.
  • pin केलेली रिपॉझिटरीयेथे पाहिलेला सूची, हस्तलिखित फाइल्स आणि पुरावा रचना देते. पूर्ण फाइल यादी व हस्तलिखित नकाशावरून संख्या घेतल्या; निवडक औपचारिक फाइल्स न चालवता वाचल्या. रचना समजण्यासाठी आढाव्याचा LaTeX स्रोत पाहिला.
  • Lean validation referenceपुरावा तपासणीचा अर्थ व मर्यादा सांगतो. 4.35.0-rc3 reference वापरला; OpenAI प्रकल्प Lean 4.34.1 pin करतो.
  • Comparator दस्तऐवजchallenge व solution फाइल्स, वातावरणाच्या गरजा आणि सशर्त हमी स्पष्ट करतात. या संग्रहासाठी सत्यापनाचा निकाल देत नाहीत.
  • Kingy.ai वरील Curtis Pyke यांचे परीक्षणप्रकाशनाचे स्वतंत्र स्थिर परीक्षण देते. स्वतंत्र Lean execution झाले नाही असे ते स्पष्ट नमूद करते; आम्ही त्याला पुरावा तपासणीची पुनरावृत्ती मानत नाही.
  • AI गणितावरील BIG CHANGEचा आधीचा अहवालमे ते सप्टेंबरमधील क्रम समाविष्ट करतो. हा लेख नव्या संग्रहाच्या artifact रचनेचा आणि तपासणी प्रक्रियेचा अभ्यास करतो.