Axiom Math का AI Lean में 246 प्राइम‑गैप्स प्रमेय को सत्यापित करता है

Axiom Math कहता है कि उसका AxiomProver सिस्टम ने प्राइम संख्याओं के अंतर पर ज्ञात सबसे मजबूत परिणाम का मशीन‑चेक्ड Lean 4 प्रमाण तैयार किया है: वह प्रमेय कि अनंत संख्या में प्राइम युग्म 246 से अधिक अंतर नहीं रखते। कंपनी ने यह परिणाम 17 अगस्त 2026 को एक इंटरैक्टिव फॉर्मलाइज़ेशन ब्लूप्रिंट के रूप में प्रकाशित किया, जिसमें 41 नामित गणितीय, इंजीनियरिंग और प्रमुख‑शोधकर्ता योगदानकर्ताओं का श्रेय दिया गया, और IEEE Spectrum first reporting ने इस मील का पत्थर पहली बार रिपोर्ट किया।

246 की सीमा द्विप्राइम अनुमान पर मानव ज्ञान की वर्तमान सीमा है, जो 19वीं सदी का सिद्धांत है कि दो के अंतर वाले प्राइम हमेशा दोहराते हैं। Axiom Math’s project page इस कार्य को जेम्स मेनार्ड के 2013 के पेपर “Small gaps between primes” की एकीकृत फॉर्मलाइज़ेशन के रूप में वर्णित करता है, साथ ही Polymath8b सहयोग के उस भाग के साथ जिसने मेनार्ड की 600 की सीमा को 246 तक घटाया। मशीन‑चेक्ड प्रमाणों को सार्वजनिक Lean लाइब्रेरी PrimeGapsLib में व्यवस्थित किया गया है, जिसमें 246 का प्रमेय उसका प्रमुख परिणाम है।

“यह प्रमेय वर्तमान में प्राइम संख्याओं के बारे में मानव ज्ञान की सीमा को दर्शाता है,” केन ओनो, Axiom Math के संस्थापक गणितज्ञ ने कहा।

औपचारिक सत्यापन का अर्थ है प्रमाण को ऐसी भाषा में अनुवादित करना जिसे एक छोटा, विश्वसनीय प्रोग्राम (जिसे कर्नेल कहा जाता है) पंक्ति दर पंक्ति जांच सके। परिणाम पूर्ण गारंटी नहीं है — कथन स्वयं को सही ढंग से अनूदित होना चाहिए, और चेकर को सटीक होना चाहिए — लेकिन यह मानव रेफरी की त्रुटिपूर्णता को श्रृंखला से हटाता है। अब तक, गणित बेंचमार्क पर प्रतिस्पर्धा करने वाले AI सिस्टम मुख्यतः छोटे, स्वतंत्र प्रमाणों वाले प्रतियोगिता समस्याओं पर मापे गए हैं; उन परिणामों और शोध‑स्तर फॉर्मलाइज़ेशन के बीच का अंतर बड़ा रहा है, जैसा कि earlier systems that excelled at olympiad geometry में देखा गया जो शोध गणित को अधिकांशतः अनछुआ छोड़ देता था।

70 मिलियन से 246 तक

यह अनुमान स्वयं, 19वीं सदी में अल्फ़ोंस डी पोलीग्नैक द्वारा सटीक रूप से सूत्रित, अभी तक प्रमाणित नहीं हुआ है। किसी भी प्रकार की पहली सीमित सीमा 2013 में आई, जब यितांग झांग ने सिद्ध किया कि अनंत संख्या में प्राइम युग्म 70 मिलियन के भीतर आते हैं। कुछ महीने बाद, मेनार्ड ने एक परिष्कृत सिव विधि प्रस्तुत की और सीमा को 600 तक घटाया — यह कार्य उनके 2022 के फील्ड्स मेडल में योगदान देता है — और Polymath8b सहयोग, जिसमें मेनार्ड और टेरेंस ताओ शामिल थे, ने इसे 246 तक पहुँचाया। Axiom Math का ब्लूप्रिंट इस प्रगति को उस परियोजना के रूप में प्रस्तुत करता है जिसे उसने फॉर्मलाइज़ करने का लक्ष्य रखा था।

फॉर्मलाइज़ेशन एक पाइपलाइन का अनुसरण करता है जिसे कंपनी तीन चरणों में वर्णित करती है। शोधकर्ताओं ने पहले प्रमाण को एक ब्लूप्रिंट के रूप में लिखा — प्रत्येक परिभाषा, लेम्मा और प्रमेय को एक लेबल, सटीक कथन और उन परिणामों की सूची दी गई जिन पर वह निर्भर करता है — जिससे एक निर्भरता ग्राफ बनाकर कार्य का क्रम निर्धारित हुआ। AxiomProver, कंपनी का मल्टी‑एजेंट सिस्टम जो औपचारिक प्रमाण के माध्यम से गणितीय शोध करता है, ने फिर Mathlib (समुदाय गणित लाइब्रेरी) और PrimeNumberTheoremAnd (एलेक्स कॉन्टोरोविच और ताओ द्वारा नेतृत्वित मौजूदा फॉर्मलाइज़ेशन प्रोजेक्ट) पर आधारित मशीन‑चेकेबल Lean 4 प्रमाण उत्पन्न किए। Axiom की टीम ने उत्पन्न कोड की समीक्षा की और इसे PrimeGapsLib में व्यवस्थित किया।

लाइब्रेरी के घोषित मुख्य परिणाम मुख्य प्रमेय से थोड़ा आगे हैं। 246 की सीमा के साथ, यह मेनार्ड की 600 की सीमा को भी फॉर्मलाइज़ करता है, और इसमें एक स्व‑निहित सत्यापन चुनौती शामिल है — केवल Mathlib पर निर्मित, प्रमाण स्लॉट खाली छोड़ा गया — जिससे Lean कंपेरेटर टूल वाले कोई भी स्वतंत्र रूप से पुष्टि कर सके कि लाइब्रेरी के प्रमाण घोषित प्रमेयों से मेल खाते हैं। कंपनी चेतावनी देती है कि पूर्ण जाँच में कई घंटे लग सकते हैं; अन्य दो परिणामों को कवर करने वाला संक्षिप्त संस्करण कुछ मिनटों में चल जाता है।

AI फॉर्मलाइज़ेशन दावों में यह कहाँ स्थित है

यह परिणाम AI सिस्टमों द्वारा शोध‑स्तर गणित करने के बढ़ते दावों के एक वर्ष में सामने आया, जिनमें से अधिकांश प्रतियोगिता स्कोर या छोटे प्रमाणों पर आधारित हैं। Axiom Math सबसे आक्रामक दावेदारों में से एक रहा है: AxiomProver को पहले से खुले समस्याओं को हल करने का श्रेय दिया गया है, जिसमें कंपनी के द्वारा सह‑समीक्षित जर्नलों में प्रकाशित कार्य भी शामिल हैं, और AI systems have now solved several long-standing Erdős problems। 246 फॉर्मलाइज़ेशन एक अलग प्रकार का परिणाम है — नया प्रमेय नहीं, बल्कि आधुनिक संख्या सिद्धांत में सबसे तकनीकी रूप से कठिन प्रमाणों में से एक का मशीन‑चेक्ड पुनर्निर्माण।

सबसे निकट तुलना इस वर्ष की शुरुआत में हुई, जब Math, Inc. ने अपने Gauss एजेंट का उपयोग करके मैरिना वियाज़ोव्स्का के फ़ील्ड्स मेडल‑विजेता स्फीयर‑पैकिंग परिणामों (आयाम 8 और 24) का औपचारिक प्रमाण पूरा किया। सिद्धार्थ हरिहरन, कार्नेगी मेलॉन के पीएच.डी. छात्र जिन्होंने उस फॉर्मलाइज़ेशन पर मानव ब्लूप्रिंट प्रयास का नेतृत्व किया और अब Axiom Math में इंटर्न तथा 246 प्रोजेक्ट के नामित गणितीय योगदानकर्ता हैं, तर्क देते हैं कि नया परिणाम अधिक व्यापक उपलब्धि है। उनका तर्क, जैसा उन्होंने बताया, यह है कि Axiom पुनः उपयोग के लिए बनाया गया है: एकल प्रमाण की एक‑बार की फॉर्मलाइज़ेशन के बजाय, PrimeGapsLib एक रखरखाव योग्य लाइब्रेरी है जिसमें प्राइम‑गैप परिणाम शामिल हैं, जो भविष्य के फॉर्मलाइज़ेशन कार्य और शोध को समर्थन देने के लिए बनाई गई है।

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

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

“दुनिया अब ऐसे कंप्यूटर कोड पर चलने वाली है जिसे कोई नहीं पढ़ता,” ओनो ने कहा। “AI यहाँ है और हम अब और नहीं देख सकते — प्रमाण फॉर्मलाइज़ेशन वह परीक्षण स्थल है जो वह सबसे महत्वपूर्ण चुनौती को हल करने में मदद करेगा, जिसका हम AI से सामना करेंगे।”

अभी के लिए डिलिवरेबल अधिक संकीर्ण और जाँचने योग्य है: 41 लेखकों का ब्लूप्रिंट, एक सार्वजनिक Lean लाइब्रेरी, और एक मशीन‑सत्यापित प्रमाण कि 246 अंतर के भीतर के प्राइम कभी समाप्त नहीं होते — द्विप्राइम अनुमान का सबसे निकटतम सत्यापित पड़ोसी, और वह सबसे गहरा शोध‑गणित का टुकड़ा जिसे अब तक किसी AI सिस्टम ने अंत‑से‑अंत जाँच किया है।