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 दर्ज करता है। ये प्रकाशन मेटाडेटा हैं, BIG CHANGE द्वारा चलाए गए जाँचकर्ता का परिणाम नहीं।

सार्वजनिक फ़ाइलें OpenAI खाते के बिना पढ़ी जा सकती हैं। घोषणा मॉडल को आंतरिक बताती है और कहती है कि OpenAI उसे जारी करने पर काम कर रहा है। इसलिए इन दस्तावेज़ों तक पहुँच उस मॉडल तक पहुँच साबित नहीं करती।

प्रमाण का अनुसरण करने से पहले संस्करण तय करें

यहाँ इस्तेमाल किया गया रिपॉज़िटरी स्नैपशॉट commit adc7f1241b42e322a6451854ab7e4b4c146bf78a है, दिनांक 6 अक्टूबर 2026, 21:58:50 UTC। इस पहचान वाले लिंक जाँचे गए स्नैपशॉट को सुरक्षित रखते हैं; main वाले लिंक बदलती default branch का अनुसरण करते हैं। OpenAI README वादा करती है कि सुधार या संशोधन आने पर पुराने रिलीज़ सुरक्षित रखे जाएँगे।

शुरुआत अवलोकनसे करें, जो गणितीय विषय के अनुसार परिवारों को समूहित करता है; फिर किसी शोधपत्र तक पहुँचने के लिए पांडुलिपि मानचित्र का उपयोग करें। उसकी निर्देशिका का नाम, रिपॉज़िटरी commit और दिया गया उद्धरण सुरक्षित रखें। पांडुलिपि की तारीख और सार्वजनिक संग्रह की रिलीज़ तारीख अलग हो सकती हैं।

परिवार 003 में एक शोधपत्र 7/8 के दाईं ओर शून्य-मुक्त क्षेत्र का दावा करता है, 11/12 के दाईं ओर के क्षेत्र के लिए वैकल्पिक प्रमाण देता है, और Landau–Siegel शून्यों पर अलग शोधपत्र है। पहले शोधपत्र की निर्देशिका 30 सितंबर की तारीख़ देती है और BibTeX उद्धरण उपलब्ध कराती है। विशिष्ट शोधपत्र दर्ज करने से इन दावों का अंतर बना रहता है।

इसका Lean दायरा पृष्ठ बताता है कि औपचारीकरण किन कथनों को कवर करता है, क्या बाहर है और शोधपत्र के बाद के अनुप्रयोग छोड़े गए हैं। यह zeta परिणाम, Dirichlet और Hecke L-functions तथा वास्तविक शून्यों के एकसमान अंतराल के लिए अलग-अलग जाँच कथनों से जोड़ता है। एक चुने हुए कथन की जाँच उस पृष्ठ की हर चीज़ का प्रतिनिधित्व नहीं करती।

चुने हुए कथन को उसकी व्यवस्था तक देखें

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

व्यवस्था एक challenge module और अलग solution module की ओर संकेत करती है। यह मानक axioms propext , Quot.sound और Classical.choice की अनुमति देती है और enable_nanoda को false पर सेट करती है। Nanoda स्वतंत्र checker है जिसका उपयोग Comparator कर सकता है; यह दी गई व्यवस्था उसे सक्षम नहीं करती।

यह challenge फ़ाइल में sorry है, जो अधूरे प्रमाण के लिए Lean placeholder है। यहाँ इसकी भूमिका स्पष्ट है: मिलान किया जाने वाला कथन देना। Comparator दस्तावेज़ challenge में placeholder की अनुमति देता है और solution में सही प्रमाण माँगता है। केवल challenge में sorry मिलने से यह पता नहीं चलता कि अलग solution पास होगा। Comparator दस्तावेज़.

दस्तावेज़ीकृत स्थानीय जाँच के लिए इस व्यवस्था, उसके challenge और solution modules तथा उनकी dependencies की ज़रूरत होती है। रिपॉज़िटरी Lean 4.34.1को pin करती है। इसका Lake manifest dependency संशोधन दर्ज करता है, जिसमें 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 लागत नहीं मापी।

सफल जाँच को उसके घोषित दायरे में पढ़ें

Lean का validation reference, जिसे देखते समय संस्करण 4.35.0-rc3 था, औपचारिक प्रमाण की स्वीकृति और प्रमेय के अर्थ की व्याख्या में अंतर करता है। दस्तावेज़ का यह संस्करण रिपॉज़िटरी के pin किए toolchain से अलग है।

सफल basic check का अर्थ है कि kernel ने परिभाषाओं, imports और axioms के अधीन औपचारिक कथन स्वीकार किया। Dependencies में अधूरे प्रमाण हो सकते हैं। Lean इस्तेमाल हुए axioms दिखाने के लिए #print axioms का वर्णन करता है, जिनमें dependency chain के अधूरे प्रमाण के लिए sorryAx शामिल है।

अधिक कठोर जाँचें संग्रहीत प्रमाण फिर चला सकती हैं या solution की तुलना अलग से निर्धारित कथन से कर सकती हैं। वे भी जाँच वातावरण और इच्छित अर्थ की सही अभिव्यक्ति पर निर्भर करती हैं। इसलिए सटीक challenge, अनुमत axioms और बाहरी checker सेटिंग को सत्यापन रिपोर्ट में दर्ज करें। Kernel की स्वीकृति या challenge से मेल जर्नल की स्वीकृति या पांडुलिपि के हर दावे के औपचारीकरण को साबित नहीं करता।

compute आँकड़ा निर्माण बताता है

OpenAI कहता है कि औसत परिणाम के लिए ChatGPT Pro में लगभग तीन घंटे सोचने के बराबर computing effort लगा। README बताती है कि evaluation में लगभग 4,000 समस्याएँ दी गईं, फिर outputs को समूहित करके महत्त्वपूर्ण चुना गया। सामान्य प्रक्रिया के अपवाद भी बताए गए हैं। ये कंपनी के generation आँकड़े हैं; ये पाठक की Lean जाँच की कीमत या कुल डॉलर बिल नहीं बताते। रिलीज़ घोषणा, generation विवरण.

परिवार 003 के लिए यह निरीक्षण एक विशिष्ट zeta कथन, प्रस्तावित solution और checker द्वारा अनुमत axioms पहचानता है। यह भी स्थापित करता है कि दिए उदाहरण में Nanoda बंद है। इस व्यवस्था की जाँच सफल होती है या नहीं, यह चलाकर दर्ज करना होगा।

स्रोत और आगे पढ़ें

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