जो संख्या मायने रखती है वह है 460,000: formally checkable proof की lines, जो OpenAI ने 1 अगस्त को गणित और theoretical computer science में दस दावे किए गए advances के समर्थन में एक public GitHub repository में डालीं। उन्हें घोषित करने वाली post, उसी सुबह की dated, कहती है कि results Astra के एक internal version से आए, जिसे वह 'हमारा अगला major model' कहती है। दसों results के साथ एक Lean certificate है, machine-checkable formal proof, github.com/openai/ten-proofs में Apache-2.0 license के तहत। हमने files जाँचीं: दसों Lean 4.32 और mathlib के साथ compile होती हैं, और किसी में 'sorry' placeholder या custom axiom नहीं है, दो सामान्य escape hatches।
दस, जैसे OpenAI बताती है: high-dimensional sphere packing के लिए Cohn-Elkies threshold तक नई upper bounds; binary और spherical codes के लिए exponentially improved bounds; non-sofic groups की construction; Connes की rigidity conjecture को झुठलाने वाला counterexample; permanent के लिए lower bounds, जिसमें log n पर n की चौथाई power का arithmetic-formula bound; quantum games के लिए exponential parallel-repetition theorem; closest vector problem के लिए polynomial-factor hardness; Ehrhart के volume conjecture का sharp जवाब; multicolor triangle Ramsey numbers के लिए superexponential lower bound, जो Erdos problem 183 सुलझा देगा; और compactness व degeneracy conjectures के counterexamples, जो Erdos problems 146 और 180 सुलझाते हैं। OpenAI का framing है कि हर problem कम से कम एक दशक से अटका था। यह framing उनका है, और Sol API rates पर करीब $2,000 compute का आँकड़ा भी।
यहाँ वह है जो आज independently verifiable है, और यह कुछ से ज़्यादा और proof से कम है। Verifiable: repository मौजूद है, दसों Lean files मौजूद हैं, contents जैसा बताया गया वैसा है, दो companion PDFs (paper और model की reasoning walkthroughs) download होते हैं, और repo में independent kernel checking की configurations हैं। अभी verifiable नहीं: OpenAI से बाहर किसी ने proofs को rebuild करने की सूचना नहीं दी है; किसी human mathematician ने उनकी समीक्षा नहीं की है; और कोई expert पुष्टि नहीं करता कि formalized statements informal theorems जैसा ही कहते हैं, वह कदम जहाँ formalization चुपचाप टूट सकता है। सबसे मज़बूत not-yet-ratified signal: erdosproblems.com, reference tracker, अब भी problem 183 को $250 prize के साथ open सूचीबद्ध करता है, जबकि एक छोटे tracker ने इसे 1 अगस्त को solved मार्क कर दिया। उस site के maintainer Thomas Bloom ने इस घोषणा को 'बड़ी ख़बर' और constructions के लिए 'बड़ा' कहा, The Decoder द्वारा उद्धृत posts में; हम उन्हें सीधे retrieve नहीं कर सके।
नाम पर, precision मायने रखती है क्योंकि यही वह article है जिसे लोग वापस link करेंगे। Blog कहता है 'Astra का एक internal version, हमारा अगला major model'। 'अगली major model family' वाक्य OpenAI researcher Noam Brown का है, जिन्होंने जोड़ा, 'दुर्भाग्य से कोई Millennium problems नहीं (अभी)', और नोट किया कि model अन्य major problems पर असफल रहा। बाक़ी सब reported है, confirmed नहीं: The Information, The Decoder के माध्यम से, Astra को Sol, Terra और Luna के साथ एक नई class बताता है, GPT-6 बनाम GPT-5.7 का फ़ैसला अनिर्णीत और कोई release date नहीं। OpenAI का अपना ethics note पूरा उद्धृत करने लायक़ है: 'पूरी तरह AI system द्वारा generated proof के लिए human authorship का दावा करना system के योगदान और genuine human intellectual work की प्रकृति दोनों को गलत ठहराएगा', और company कहती है कि वह correctness की ज़िम्मेदारी लेती है जबकि arguments model-generated थे। rebuilds आने पर उन्हें इसी वाक्य से पकड़ना होगा।