1976 में इलिनॉय के दो गणितज्ञों ने घोषणा की कि उन्होंने सिद्ध कर दिया है कि किसी भी नक्शे को रंगने के लिए चार रंग काफ़ी हैं, और उनके प्रमाण का एक हिस्सा सिर्फ़ कंप्यूटर ही जाँच सकता था। बहुत-से गणितज्ञ बेचैन हो गए: अगर कोई इंसान इसे पूरा पढ़ ही नहीं सकता, तो क्या यह सचमुच प्रमाण है? पचास साल बाद यह प्रश्न उलट गया है। 2026 में AI प्रणालियों ने उन परिणामों के मुख्य विचार खोजे जिन्हें विशेषज्ञ दशकों तक नहीं खोज पाए थे। यह लेख यह कहानी क्रम से सुनाता है और हर मशहूर समस्या के लिए ठीक-ठीक बताता है कि मशीन ने क्या किया, क्योंकि “कंप्यूटर से सुलझा” के मायने बहुत अलग हो सकते हैं।
वह अंतर जिसे छात्र अक्सर भ्रमित कर देते हैं
किसी प्रमाण में कंप्यूटर की तीन बिल्कुल अलग भूमिकाएँ
- मामलों की जाँच: इंसान समस्या को एक लंबी लेकिन सीमित सूची में बदल देता है, और कंप्यूटर हर मद जाँचता है (चार रंग, केप्लर)।
- प्रमाण की खोज: कंप्यूटर ख़ुद तर्क ढूँढ लेता है (रॉबिन्स, और 2026 के AI परिणाम)।
- प्रमाण का सत्यापन: Coq या Lean जैसा प्रमाण-सहायक किसी प्रमाण के हर तार्किक कदम की पुष्टि करता है, चाहे उसे किसी ने भी लिखा हो।
1976: चार रंग, और एक ऐसा प्रमाण जिसे कोई पढ़ नहीं सकता था
GCSE मूल
प्रश्न इतना आसान है कि प्राथमिक स्कूल का बच्चा भी समझ ले: नक्शे को ऐसे रंगिए कि पड़ोसी देशों का रंग कभी एक न हो। कितने रंगों की ज़रूरत पड़ सकती है? फ़्रांसिस गथरी ने 1852 में अनुमान लगाया: चार। यह देखना आसान है कि चार की ज़रूरत पड़ सकती है (नीचे का चित्र देखें), लेकिन यह सिद्ध करना कि हर संभव नक्शे के लिए चार रंग हमेशा काफ़ी हैं, गणितज्ञों से 124 साल तक नहीं हुआ।
चित्रण: चार रंगों की ज़रूरत क्यों पड़ सकती है
केनेथ एपेल और वोल्फ़गैंग हाकेन ने यह दिखाने का तरीक़ा खोजा कि पाँच रंग माँगने वाले किसी भी नक्शे में लगभग दो हज़ार ख़ास पैटर्नों में से कोई एक ज़रूर होगा, और इनमें से हर पैटर्न को “घटाकर” हटाया जा सकता है। सबको हाथ से जाँचना असंभव था, इसलिए यह काम कंप्यूटर ने किया, एक हज़ार घंटे से ज़्यादा के कंप्यूटर समय में। प्रमेय सिद्ध हो गया, पर इस तरह कि व्यवहार में “प्रमाण” का अर्थ ही बदल गया।
शंका कैसे दूर हुई: 1996 में एक छोटा कंप्यूटर-प्रमाण आया, और 2005 में जॉर्ज गोंतिए और बेंजामिन वर्नर ने पूरे तर्क को प्रमाण-सहायक Coq में सत्यापित किया। आज यह गणित के सबसे गहराई से सत्यापित प्रमेयों में से एक है।
1996: पहला प्रमाण जो कंप्यूटर ने ख़ुद खोजा
स्नातक विस्तार
रॉबिन्स अनुमान यह पूछता था कि क्या तीन छोटे नियम ठीक वही बीजगणित बताते हैं जो बूलियन बीजगणित बताता है, यानी हर कंप्यूटर चिप के भीतर का सत्य/असत्य तर्क। अल्फ़्रेड टार्स्की समेत शीर्ष तर्कशास्त्री साठ साल तक इसे हल नहीं कर पाए थे। 1996 में विलियम मैक्यून के स्वचालित प्रमेय-प्रमाणक EQP ने लगभग आठ दिनों तक संभावित तर्क-श्रृंखलाएँ खोजीं और एक प्रमाण पा लिया। यह 1976 से अलग किस्म की बात थी: किसी ने कंप्यूटर को नहीं बताया था कि तर्क कैसा दिखना चाहिए।
1998–2014: केप्लर के संतरे
1611 में योहानेस केप्लर ने दावा किया कि फल वाले जिस तरह संतरे सजाते हैं (हर परत नीचे वाली परत के गड्ढों में), वही बराबर गोलों को सबसे घना भरने का तरीक़ा है। यह लगभग 74% जगह भर देता है (ठीक-ठीक π/√18)।
चित्रण: फल वाले का ढेर
इस व्यवस्था का घनत्व: π / √18 ≈ 74.05% जगह भरी
थॉमस हेल्स ने सैमुअल फ़र्ग्युसन के साथ इस प्रश्न को हज़ारों अनुकूलन समस्याओं में बदला, उन्हें कंप्यूटर से हल किया और 1998 में प्रमाण की घोषणा की। पत्रिका के समीक्षकों ने कहा कि वे “99% आश्वस्त” हैं कि यह सही है, पर हर गणना नहीं जाँच सकते। जवाब में हेल्स ने Flyspeck परियोजना चलाई ताकि सब कुछ प्रमाण-सहायक सॉफ़्टवेयर में दोबारा सत्यापित हो; यह 2014 में पूरी हुई।
2016: 200 टेराबाइट का प्रमाण
GCSE मूल
यह एक पहेली है जिसे आप ख़ुद आज़मा सकते हैं। हर पूर्ण संख्या को लाल या नीला रंगिए। क्या आप ऐसा कर सकते हैं कि कोई भी पाइथागोरियन त्रिक (तीन संख्याएँ जिनमें a² + b² = c², जैसे 3, 4, 5) एक ही रंग की न हो?
ख़ुद आज़माइए: 1 से 40 को ऐसे रंगें कि कोई पाइथागोरियन त्रिक एक रंग की न हो
किसी संख्या पर टैप करके उसे नीले और लाल के बीच बदलें। लक्ष्य: कोई भी त्रिक a² + b² = c² (जैसे 3, 4, 5) पूरी एक रंग की नहीं होनी चाहिए। टकराव वाली त्रिक की संख्याओं पर गहरा घेरा आता है।
16 एक-रंगी त्रिकें: 3–4–5, 5–12–13, 6–8–10, 7–24–25…
रोनाल्ड ग्राहम ने उत्तर के लिए 100 डॉलर का इनाम रखा था। 2016 में मारेन ह्यूले, ओलिवर कुलमान और विक्टर मारेक ने सुपरकंप्यूटर Stampede पर लगभग दो दिन एक SAT सॉल्वर (बहुत बड़ी सत्य/असत्य तार्किक पहेलियाँ हल करने वाला सॉफ़्टवेयर) चलाया। उत्तर: 1 से 7,824 तक की हर संख्या सुरक्षित ढंग से रंगी जा सकती है, पर 1 से 7,825 तक नहीं। इस बात का प्रमाण कि 7,825 संख्याओं का कोई भी रंगना काम नहीं करता, 200 टेराबाइट का था, जिसे उस समय Nature ने अब तक का सबसे बड़ा गणितीय प्रमाण बताया। इसी तकनीक ने 2019 में सात आयामों में घनों से अंतरिक्ष को टाइल करने वाले केलर अनुमान का फ़ैसला किया।
त्वरित जाँच
बूलियन पाइथागोरियन त्रिक समस्या का उत्तर 7,825 है। इस संख्या का मतलब क्या है?
2025–2026: AI विचार खोजने लगा
स्नातकोत्तर विस्तार
ऊपर की हर बात में कंप्यूटर का इस्तेमाल जाँचने के लिए, या इंसानों के बनाए ढाँचे के भीतर खोजने के लिए हुआ। 2025 से बड़े भाषा मॉडलों पर आधारित प्रणालियाँ ख़ुद गणितीय विचार सुझाने लगीं, और उन्हें प्रमाण-सहायक Lean के साथ जोड़ने लगीं, ताकि परिणाम पर सिर्फ़ भरोसा करने के बजाय मशीन से उसकी जाँच हो सके।
इकाई दूरी अनुमान (मई 2026)। 1946 में पॉल एर्डोश ने पूछा: अगर आप एक समतल सतह पर n बिंदु रखें, तो कितने जोड़े ठीक 1 इकाई की दूरी पर हो सकते हैं? उनका मानना था कि उत्तर n से बस थोड़ा-सा तेज़ बढ़ता है। OpenAI के एक आंतरिक मॉडल ने बीजीय संख्या सिद्धांत के गहरे औज़ारों से बिंदु-समुच्चयों का एक अनंत परिवार खोजा जो इसे n की एक वास्तविक घात से पार कर जाता है। फ़ील्ड्स मेडल विजेता टिमोथी गावर्स और जैकब त्सिमरमैन समेत नौ शीर्ष गणितज्ञों ने इसे जाँचा और एक साथी शोधपत्र लिखा, और विल सॉविन ने इस बढ़त को स्पष्ट रूप में लिखा। गिल कलाई ने इसके महत्व की तुलना 1976 के चार रंग प्रमाण से की।
चित्रण: इकाई दूरियाँ गिनना
19 बिंदु, ठीक 1 इकाई दूर वाले 42 जोड़े
AlphaProof Nexus (मई 2026)। Google DeepMind ने अपने एजेंट को, जो Gemini मॉडल को Lean के साथ जोड़ता है, एर्डोश समस्याओं के डेटाबेस की 353 खुली समस्याओं पर लगाया। उसने 9 हल कीं, जिनमें दो 56 साल से खुली थीं, और पूर्णांक अनुक्रमों के ऑनलाइन विश्वकोश (OEIS) के 44 अनुमान सिद्ध किए। हर प्रमाण Lean में कंपाइल होता है। पर सफलता दर पर ध्यान दें: लगभग 2.5%।
Astra (अगस्त 2026)। OpenAI ने अपने अगले, अप्रकाशित मॉडल के दस परिणामों की घोषणा की, जिनमें नॉन-सोफ़िक समूह की पहली रचना (मिखाइल ग्रोमोव के 1999 में उठाए प्रश्न का उत्तर), एर्डोश की तीन समस्याएँ और 1978 के बाद पहली बार गोलों को भरने की एक सामान्य सीमा में सुधार शामिल थे। हर परिणाम के साथ Lean प्रमाणपत्र था। एक स्वतंत्र मानवीय ऑडिट को मुख्य परिणामों में कोई पुष्ट बड़ी ग़लती नहीं मिली, हालाँकि एक परिणाम पर एक विशेषज्ञ ने बड़े संशोधन का अनुरोध किया, और लिखते समय तक पत्रिकाओं की सहकर्मी-समीक्षा पूरी नहीं हुई थी।
वह अंतर जिसे छात्र अक्सर भ्रमित कर देते हैं
“AI ने सुलझा दिया” वाली हर सुर्ख़ी सच नहीं होती
पचास साल, एक समय-रेखा में
चित्रण: प्रमाणों में मशीनों के पचास साल, 1976–2026
- 1976 — चार रंग प्रमेय
- 1994 — फ़र्मा का अंतिम प्रमेय
- 1996 — रॉबिन्स अनुमान
- 1998 — केप्लर अनुमान
- 2016 — बूलियन पाइथागोरियन त्रिकें
- 2019 — केलर अनुमान (आयाम 7)
- 2025 — त्रिविमीय काकेया
- 2026 — ग्राहम का पुनर्व्यवस्था अनुमान
- 2026 — एर्डोश की इकाई दूरी (खंडित)
- 2026 — नॉन-सोफ़िक समूह (Astra, घोषित)
समयरेखा
- 1976एपेल और हाकेन 1,000 घंटे से ज़्यादा की कंप्यूटर जाँच से चार रंग प्रमेय सिद्ध करते हैं: पहला मशहूर कंप्यूटर-सहायित प्रमाण।
- 1996विलियम मैक्यून का स्वचालित प्रमाणक EQP लगभग आठ दिनों में ख़ुद रॉबिन्स अनुमान का प्रमाण खोज लेता है।
- 1998थॉमस हेल्स केप्लर अनुमान (गोलों को भरना) के कंप्यूटर-सहायित प्रमाण की घोषणा करते हैं।
- 2005गोंतिए और वर्नर पूरे चार रंग प्रमाण को प्रमाण-सहायक Coq में सत्यापित करते हैं।
- 2014Flyspeck परियोजना केप्लर अनुमान का पूरी तरह मशीन-सत्यापित प्रमाण पूरा करती है।
- 2016एक SAT सॉल्वर बूलियन पाइथागोरियन त्रिक समस्या का फ़ैसला करता है: उत्तर 7,825, 200 TB के प्रमाण के साथ।
- 2019आयाम 7 में केलर अनुमान का फ़ैसला SAT से होता है: यह आख़िरी खुला आयाम था।
- अक्टूबर 2025GPT-5 द्वारा एर्डोश की दस समस्याएँ “हल” करने के दावे वापस लिए जाते हैं: हल पहले से साहित्य में मौजूद थे।
- मई 2026OpenAI का एक मॉडल एर्डोश का 1946 का इकाई दूरी अनुमान खंडित करता है; DeepMind का AlphaProof Nexus Lean में एर्डोश की 9 खुली समस्याएँ हल करता है।
- अगस्त 2026OpenAI अपने अप्रकाशित मॉडल Astra के दस परिणाम Lean प्रमाणपत्रों के साथ घोषित करता है, जिनमें पहला नॉन-सोफ़िक समूह शामिल है।
अगर आप गणित सीख रहे हैं तो इसका क्या मतलब है
इस लेख का हर परिणाम फिर भी इंसानों पर निर्भर था: किसी को समस्या को सटीक रूप से रखना था, तय करना था कि कौन-सा तरीक़ा आज़माने लायक़ है, जाँचना था कि कंप्यूटर ने जो प्रमेय सिद्ध किया वही असल में मायने रखता है, और समझाना था कि वह सच क्यों है। ठीक यही कौशल स्कूल का गणित तब बनाता है जब वह आपसे हल के चरण दिखाने को कहता है, और यही हमारे लेख क्या AI सच में गणित कर सकता है? का विषय है। अब भी खुली समस्याओं के लिए, और इन सुलझी समस्याओं की कार्ड-दर-कार्ड सूची के लिए, हमारा अनसुलझी गणितीय पहेलियों का केंद्र देखें।
स्रोत और आगे पढ़ने के लिए
- Four colour theorem — Wikipedia
- Robbins algebra — Wikipedia
- Hales et al., A formal proof of the Kepler conjecture (Forum of Mathematics, Pi, 2017)
- Two-hundred-terabyte maths proof is largest ever — Nature (2016)
- Keller's conjecture — Wikipedia
- Gil Kalai — Erdős' Unit Distance Problem was Disproved (21 May 2026)
- Advancing Mathematics Research with AI-Driven Formal Proof Search (AlphaProof Nexus, arXiv:2605.22763)
- OpenAI — Ten advances in mathematics and theoretical computer science (1 Aug 2026)
- Sienicki & Sienicki, A Human Audit of OpenAI's AI-Generated Mathematical Proofs (arXiv:2608.14673)
- The Decoder — a GPT-5 math breakthrough that never happened (Oct 2025)
अंतिम जाँच: 3 अक्टूबर 2026। AI के परिणाम तेज़ी से बदलते हैं; ताज़ा स्थिति के लिए ऊपर दिए स्रोत देखें।
अक्सर पूछे जाने वाले प्रश्न
क्या कंप्यूटर-सहायित प्रमाण “असली” प्रमाण है?
हाँ: तर्क किसी भी प्रमाण जैसा ही है; कंप्यूटर बस ऐसे कदम उठाता है जो किसी इंसान के लिए बहुत ज़्यादा या बहुत लंबे हैं। असली सवाल यह है कि कैसे जाँचें कि कंप्यूटर ने वे कदम सही उठाए। इसीलिए चार रंग और केप्लर के प्रमाण बाद में प्रमाण-सहायकों में दोबारा सत्यापित किए गए (2005 में Coq और 2014 में Flyspeck परियोजना), जो हर तार्किक कदम को यांत्रिक रूप से जाँचते हैं।
क्या AI ने सच में खुली गणितीय समस्याएँ हल की हैं, या यह बढ़ा-चढ़ाकर कही बात है?
दोनों हुआ है। असली परिणामों में मई 2026 में एर्डोश के इकाई दूरी अनुमान का खंडन (जिसे साथी शोधपत्र लिखने वाले नौ शीर्ष गणितज्ञों ने जाँचा) और DeepMind के AlphaProof Nexus द्वारा आज़माई गई 353 में से 9 खुली एर्डोश समस्याओं को मशीन-सत्यापित Lean प्रमाणों के साथ हल करना शामिल है। लेकिन अक्टूबर 2025 में GPT-5 द्वारा एर्डोश की दस समस्याएँ हल करने के दावे पहले से प्रकाशित हलों की दोबारा खोज निकले, और पोस्ट हटा दी गईं। स्थिति की जाँच: 3 अक्टूबर 2026।
Lean क्या है, और गणित में AI के लिए यह क्यों मायने रखता है?
Lean एक “प्रमाण-सहायक” है: एक प्रोग्रामिंग भाषा जिसमें प्रमाण इतनी सटीकता से लिखा जाता है कि कंप्यूटर हर कदम जाँच सके। अगर कोई AI अपना प्रमाण Lean में लिखे और वह कंपाइल हो जाए, तो आपको AI पर भरोसा करने की ज़रूरत नहीं रहती, बस उस छोटे, अच्छी तरह परखे गए जाँचकर्ता पर और इस बात पर कि प्रमेय का कथन वही कहता है जो आप समझते हैं। इसीलिए 2026 के ज़्यादातर गंभीर AI गणित परिणाम Lean प्रमाणों के साथ आते हैं।
क्या AI गणितज्ञों की जगह ले लेगा?
आज के प्रमाणों के आधार पर नहीं। 2026 की सबसे मज़बूत प्रणालियाँ भी आज़माई गई खुली समस्याओं में से छोटा-सा हिस्सा ही हल करती हैं (AlphaProof Nexus: आज़माई गई एर्डोश समस्याओं का लगभग 2.5%), और प्रश्न चुनना, कथन जाँचना, परिणामों की व्याख्या करना और उनके इर्द-गिर्द सिद्धांत बनाना अब भी इंसान ही करते हैं। जो तेज़ी से बदल रहा है, वह यह है कि खोज और जाँच का कितना हिस्सा मशीनों को सौंपा जा सकता है।
पाठकों की रेटिंग और समीक्षाएँ
इस लेख को कई अलग-अलग पहलुओं पर रेट करें — आपकी रेटिंग दूसरे पाठकों की मदद करती है, और हमें बेहतर बनाने में मदद करती है।
क्या यह लेख उपयोगी था?
हमें अपनी राय बताएं — कोई सुधार, कोई सवाल जिसका जवाब नहीं मिला, या कोई विषय जिसे आप अगली बार कवर होते देखना चाहते हैं।
बात करना पसंद करेंगे? अपनी सुविधा के समय पर मुफ़्त वीडियो कॉल बुक करें: छोटे सवाल के लिए 15 मिनट, बाकी के लिए 30 मिनट। समय आपके अपने टाइम ज़ोन में दिखता है।
लेखक के बारे में
Sudershan Soni
मोस्तक सर्विसेज़ में संस्थापक व मुख्य शिक्षक — MSc-योग्य गणित, विज्ञान, कंप्यूटर साइंस और STEM शिक्षक, 20+ वर्षों के पेशेवर अनुभव के साथ, 11+ और GCSE से A-Level और उससे आगे तक के छात्रों को दुनिया भर में ऑनलाइन पढ़ाते हैं।
पूरी प्रोफ़ाइल पढ़ें