पॉँकारे, यंत्राने ओळ न् ओळ तपासलेले

सिद्धता तपासणे हे गणितातील सर्वात कष्टाच्या कामांपैकी एक आहे, विशेषतः जेव्हा एखादा युक्तिवाद अनेक क्षेत्रांमध्ये पसरलेला असतो. AI मुळे सिद्धतांची निर्मिती वेगाने होऊ लागल्यावर, विश्वासार्ह पडताळणी अधिकच महत्त्वाची ठरते. Lean 4 सारखे सिद्धता सहाय्यक (proof assistants) याचे एक उत्तर देतात: व्याख्या, विधाने आणि सिद्धता कोड म्हणून लिहिल्या जातात, आणि सॉफ्टवेअरचा एक लहान, विश्वासार्ह गाभा, त्याचा “कर्नल”, प्रत्येक पायरी तपासतो. कर्नलमधून पार झालेली सिद्धता तिचे विधान प्रस्थापित करते; माणसांसाठी उरते ते एवढेच की ते विधान गणितज्ञांना अभिप्रेत असलेलेच खरोखर सांगते का, हे तपासणे.

संक्षिप्त सिद्धता, उणी ग्रंथालय

पेरेलमन यांनी सिद्ध केलेली पॉँकारे अटकळ (Poincaré conjecture) सांगते की प्रत्येक बंदिस्त, साधे-संबद्ध (simply connected) त्रिमितीय बहुरूप (manifold) — अनौपचारिकपणे सांगायचे तर, ज्यात एखादा फास अडकू शकेल असे छिद्र नसलेले मर्यादित त्रिमितीय अवकाश — त्रिमितीय गोलाशी समतुल्य असते. ही सिद्धता रिचर्ड हॅमिल्टन (Richard Hamilton) यांनी सुरू केलेल्या रिची प्रवाह (Ricci flow) कार्यक्रमाला अनुसरते. पेरेलमन यांच्या 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 नावाच्या प्रणालीमधून, जी मर्यादित “मोहिमा” अनेक सर्व्हरकडे पाठवते. एक बॉट प्रत्येक योगदान संकलित (compile) करून स्वीकारलेली योगदाने एकत्र करत असे. विधानांचे औपचारिकीकरण आणि सिद्धतांची बांधणी यांचा बहुतेक भार GPT-6-Astra ने उचलला; Fable-5.1 चा वापर स्वतंत्र तपासण्या, अडकलेल्या कामांचे निदान आणि विधानांची समीक्षा यांसाठी झाला.

सुमारे दोन आठवड्यांत 28 लाख ओळी

महिन्यांच्या तयारीनंतर, मुख्य औपचारिकीकरणाला दोन आठवड्यांहून थोडा जास्त वेळ लागला. AI सदस्यत्वे आणि भाड्याने घेतलेले सर्व्हर यांचा खर्च सुमारे 25,000 डॉलर आला. हे काम प्रमेयाची संस्थितिक (topological) आणि मसृण (smooth) अशी दोन्ही रूपे सिद्ध करते, संपूर्णपणे संकलित होते, आणि केवळ Mathlib वापरून लिहिलेल्या लक्ष्य-विधानांविरुद्धच्या स्वतंत्र तपासणीतही उत्तीर्ण होते.

ते प्रचंड आहे: Lean च्या सुमारे 32 लाख ओळी, ज्या अंतिम प्रमेय ज्यावर अवलंबून आहे तेवढेच ठेवल्यावर 28 लाखांवर आल्या. लेखकांच्या मोजणीनुसार, जवळजवळ निम्मा भाग पार्श्वभूमीचा सिद्धांत आहे. मॉर्गन आणि टियान यांनी एकाच तळटिपेत उल्लेखलेल्या एका अभिजात निकालाला — त्रिमितीय बहुरूपांवरील मसृण संरचनांबद्दलच्या — एकट्याला सुमारे 6,50,000 ओळी लागल्या.

माणसांनी तरीही काय केले

लेखक अडथळ्यांचे तीन प्रकार करतात: गणितीय उणिवा, Lean अंमलबजावणीतील अडचणी आणि समन्वयाच्या अडचणी. माणसांनी विधानांची व्याप्ती ठरवली (उदाहरणार्थ, एखादा निकाल केव्हा त्रिमितीपुरता मर्यादित करायचा), गहाळ युक्तिवाद हेरले — जसे की एजंटांना सापडू न शकलेली एक स्थानिक संक्षिप्तता (local compactness) पायरी — आणि लपलेली गृहीतके पकडली. त्यांचा मुख्य धडा: कामाचे संघटन एजंटांच्या क्षमतेइतकेच महत्त्वाचे ठरले. Anthropic ने अलीकडे केलेल्या फर्माच्या अंतिम प्रमेयाच्या औपचारिकीकरणातूनही ते हाच निष्कर्ष काढतात; तिथेही सुरुवातीच्या प्रयत्नांत प्रकल्पाच्या स्थितीचा मागोवा सुटल्याने पुन्हा सुरुवात करावी लागली होती.

पडताळलेले, पण अजून नीटनेटके नाही

लेखक हे काम पूर्ण झाल्याचे मानत नाहीत. कोडमध्ये पुनरावृत्ती भरलेली आहे; एजंटांच्या सिद्धता नेहमी संदर्भग्रंथाचा मार्ग अनुसरत नाहीत; आणि याचे भूमितीय विश्लेषणाच्या पुन्हा वापरता येण्याजोग्या ग्रंथालयात रूपांतर करणे हे पुढचे काम आहे. दुसऱ्या एका संघाने याच अटकळीचे स्वतंत्र औपचारिकीकरणही जाहीर केले आहे. त्यांची आशा: एक दिवस एकटा गणितज्ञ अशा साधनांचा वापर करून स्वतःचे संशोधन पडताळू शकेल.

हितसंबंधांचा संघर्ष. संघाने Claude Code आणि Fable-5.1 हे मॉडेल वापरले, दोन्ही Anthropic चे, आणि त्यांच्यासोबत OpenAI सदस्यत्वांमार्फत वापरलेले GPT-6-Astra, ज्याने बहुतेक काम केले. शोधनिबंध आपल्या प्रकल्पाची तुलना Anthropic च्या फर्माच्या अंतिम प्रमेयाच्या औपचारिकीकरणाशीही करतो. हा लेख Claude ने लिहिला आहे.