पॉइनकारे, मशीन ने पंक्ति-दर-पंक्ति जाँचा

किसी प्रमाण की जाँच करना गणित के सबसे कठिन कामों में से एक है, ख़ासकर जब कोई तर्क कई क्षेत्रों में फैला हो। जैसे-जैसे AI प्रमाणों के उत्पादन को तेज़ कर रहा है, भरोसेमंद सत्यापन और ज़्यादा अहम होता जा रहा है। Lean 4 जैसे प्रूफ़ असिस्टेंट एक जवाब देते हैं: परिभाषाएँ, कथन और प्रमाण कोड के रूप में लिखे जाते हैं, और सॉफ़्टवेयर का एक छोटा भरोसेमंद केंद्र, उसका “कर्नेल”, हर क़दम जाँचता है। कर्नेल से पास होने वाला प्रमाण अपने कथन को स्थापित कर देता है; इंसानों के लिए बस यह जाँचना बचता है कि कथन सचमुच वही कहता है जो गणितज्ञों का आशय है।

एक संक्षिप्त प्रमाण, एक ग़ायब लाइब्रेरी

पेरेलमान द्वारा सिद्ध पॉइनकारे अनुमान कहता है कि हर बंद, सरल रूप से संबद्ध (सिंपली कनेक्टेड) त्रिविमीय मैनिफ़ोल्ड — अनौपचारिक रूप से, एक सीमित त्रिविमीय स्थान जिसमें कोई ऐसा छेद न हो जिसमें कोई फंदा अटक सके — त्रिविमीय गोले के समतुल्य है। प्रमाण रिचर्ड हैमिल्टन द्वारा शुरू किए गए रिक्की फ़्लो कार्यक्रम का अनुसरण करता है। पेरेलमान के 2002–2003 के तीन प्रीप्रिंट ने मुख्य तर्क बेहद संक्षिप्त रूप में दिए; इसके बाद विस्तृत विवरण आए, जिनमें John Morgan और Gang Tian का 2007 का मोनोग्राफ़ भी है, जिसका यह परियोजना अनुसरण करती है।

यह प्रमाण ज्यामितीय विश्लेषण पर टिका है, जो Lean की सामुदायिक लाइब्रेरी Mathlib में ज़्यादातर मौजूद नहीं था। नींव का बड़ा हिस्सा शून्य से बनाना पड़ा।

गणितज्ञों द्वारा स्थिर किए गए पड़ाव

पेकिंग विश्वविद्यालय और बीजिंग के अन्य संस्थानों के Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu और सहयोगियों ने मई 2026 में शुरुआत की: गणितीय प्रशिक्षण वाले तीन “AI इंजीनियर” गणितज्ञों के साथ काम कर रहे थे। उनका पहला तरीक़ा — पृष्ठभूमि सिद्धांत के बड़े हिस्सों को औपचारिक रूप देना — धीमा था, और उससे निकला कोड उनकी अपेक्षाओं पर खरा नहीं उतरा।

सितंबर 2026 में उन्होंने फिर से शुरुआत की। प्रमाण को लगभग 90 पड़ावों में काटा गया, जिनमें से हर एक अपनी ज़रूरी परिभाषाओं के साथ एक सटीक Lean कथन था। गणितज्ञों ने इन कथनों की औपचारिकता से पहले या उसके दौरान समीक्षा की, और फिर उन्हें स्थिर (फ़्रीज़) कर दिया गया: एजेंट उन्हें बदल नहीं सकते थे, और कोई भी सुधार वापस गणितज्ञों के पास जाता था। चूँकि कोई भी एजेंटों की लिखी हर पंक्ति नहीं पढ़ सकता था, ये पड़ाव वे जाँच-बिंदु बन गए जहाँ इंसानों ने गणित की पुष्टि की।

फिर एजेंटों ने समानांतर रूप से काम किया — कोडिंग टूल्स (मुख्यतः Codex और Claude Code) के साथ इंटरैक्टिव सत्रों के ज़रिए, और Archon Horizon नाम की एक प्रणाली के ज़रिए जो सीमित “मिशनों” को कई सर्वरों पर भेजती है। एक बॉट हर योगदान को कंपाइल करता था और स्वीकार किए गए योगदानों को मिला देता था। कथनों को औपचारिक रूप देने और प्रमाण बनाने का ज़्यादातर काम GPT-6-Astra ने किया; Fable-5.1 का इस्तेमाल स्वतंत्र जाँच, अटके कामों का निदान करने और कथनों की समीक्षा के लिए हुआ।

लगभग दो हफ़्तों में 28 लाख पंक्तियाँ

महीनों की तैयारी के बाद मुख्य औपचारिकीकरण में दो हफ़्ते से थोड़ा ज़्यादा लगा। AI सब्सक्रिप्शन और किराए के सर्वरों पर लगभग 25,000 डॉलर ख़र्च हुए। यह काम प्रमेय के स्थलाकृतिक और चिकने दोनों संस्करणों को सिद्ध करता है, पूरी तरह कंपाइल होता है, और सिर्फ़ Mathlib से लिखे गए लक्ष्य-कथनों के ख़िलाफ़ एक स्वतंत्र जाँच में खरा उतरता है।

यह विशाल है: Lean की लगभग 32 लाख पंक्तियाँ, जिन्हें सिर्फ़ वह रखकर 28 लाख तक छाँटा गया जिस पर अंतिम प्रमेय निर्भर करता है। लेखकों की गिनती के अनुसार, लगभग आधा हिस्सा पृष्ठभूमि सिद्धांत है। एक शास्त्रीय परिणाम जिसका Morgan और Tian सिर्फ़ एक फ़ुटनोट में ज़िक्र करते हैं — त्रिविमीय मैनिफ़ोल्ड पर चिकनी संरचनाओं के बारे में — अकेले लगभग 6,50,000 पंक्तियाँ ले गया।

इंसानों ने फिर भी क्या किया

लेखक बाधाओं को तीन तरह में बाँटते हैं: गणितीय कमियाँ, Lean में कार्यान्वयन की समस्याएँ और समन्वय की समस्याएँ। इंसानों ने कथनों का दायरा तय किया (उदाहरण के लिए, किसी परिणाम को कब तीन आयामों तक सीमित करना है), छूटे हुए तर्क पहचाने — जैसे स्थानीय संहतता (लोकल कॉम्पैक्टनेस) का एक क़दम जो एजेंट नहीं ढूँढ पाए — और छिपी मान्यताएँ पकड़ीं। उनका मुख्य सबक़: काम का संगठन उतना ही मायने रखता था जितनी एजेंटों की क्षमता। वे यही निष्कर्ष Anthropic द्वारा हाल में फ़र्मा के अंतिम प्रमेय के औपचारिकीकरण से भी निकालते हैं, जिसे भी शुरुआती प्रयासों में परियोजना की स्थिति का हिसाब खो देने के बाद फिर से शुरू करना पड़ा था।

सत्यापित, लेकिन अभी सुव्यवस्थित नहीं

लेखक इस काम को पूरा हुआ नहीं मानते। कोड दोहराव से भरा है; एजेंटों के प्रमाण हमेशा संदर्भ-मार्ग का अनुसरण नहीं करते; और इसे ज्यामितीय विश्लेषण की एक दोबारा इस्तेमाल होने लायक़ लाइब्रेरी में बदलना अगला काम है। एक और टीम ने भी इसी अनुमान के स्वतंत्र औपचारिकीकरण की घोषणा की है। उनकी उम्मीद: कि एक दिन कोई अकेला गणितज्ञ ऐसे औज़ारों से अपने ही शोध का सत्यापन कर सकेगा।

हितों का टकराव। टीम ने Claude Code और Fable-5.1 मॉडल का इस्तेमाल किया, दोनों Anthropic के हैं, साथ में OpenAI सब्सक्रिप्शन के ज़रिए इस्तेमाल किया गया GPT-6-Astra, जिसने ज़्यादातर काम किया। शोधपत्र अपनी परियोजना की तुलना Anthropic द्वारा फ़र्मा के अंतिम प्रमेय के औपचारिकीकरण से भी करता है। यह लेख Claude ने लिखा है।