वर्ष 1637 में, गणितज्ञ पियरे डी फर्माट ने समीकरण $x^n + y^n = z^n$ पर एक कथन प्रस्तावित किया, जहाँ $x$, $y$, $z$ और $n$ धनात्मक पूर्णांक हैं। फर्माट ने दावा किया कि यदि घातांक $n$ 2 से अधिक है तो इस समीकरण का कोई मान्य समाधान नहीं होगा।
इसका मतलब है कि $x$, $y$ और $z$ के मानों का ऐसा कोई संयोजन नहीं है जो इस कथन को सत्य बना सके; फर्माट के अनुसार, $x^n$ और $y^n$ का योग कभी भी $z^n$ के बराबर नहीं होगा। $n$ के 2 से अधिक होने की आवश्यकता की तुलना पाइथागोरस प्रमेय ($x^2 + y^2 = z^2$) से की जा सकती है, जो सत्य है, जैसा कि $3^2 + 4^2 = 5^2$ द्वारा उदाहरण दिया गया है, यह साबित करते हुए कि जब $n=2$ होता है तो फर्माट का खंडन लागू नहीं होता है।
फर्माट ने अनुमान लगाया कि $n=3$, $n=4$ और अन्य बड़े मानों के लिए समाधान की असंभवता बनी रहेगी, लेकिन उन्होंने अपने मन में मौजूद प्रमाण को कभी दर्ज नहीं किया। इस अवधारणा को फर्माट का अंतिम प्रमेय कहा जाता है। किसी ने फर्माट की सटीकता को सिद्ध करने में 357 साल लगाए, जिसमें एंड्रयू वाइल्स ने 1994 में प्रमाण पूरा किया, जिसे बीसवीं सदी की एक वैज्ञानिक उपलब्धि माना जाता है। इस उपलब्धि के लिए, वाइल्स को 2016 में एबेल पुरस्कार मिला।
हाल ही में, आर्टिफिशियल इंटेलिजेंस मॉडल क्लॉड के एक प्रोटोटाइप ने इस प्रदर्शन को 13 मिलियन लाइनों वाले सत्यापन योग्य कोड में बदल दिया। क्लॉड के डेवलपर, एंथ्रोपिक ने 4 सितंबर को यह घोषणा की। एआई ने परियोजना को पूरा करने में केवल 11 दिन लिए, जबकि अनुमान है कि मनुष्यों को वही काम करने में लगभग 10 साल लगेंगे।
यह ध्यान रखना महत्वपूर्ण है कि क्लॉड ने समस्या का समाधान नहीं किया, बल्कि उसके प्रमाण को औपचारिक रूप दिया। इसने मूल रूप से प्राकृतिक भाषा (शब्दों) में लिखे गए प्रदर्शन को एक औपचारिक प्रमाण में परिवर्तित कर दिया जो कम्प्यूटेशनल सत्यापन योग्य है, अनिवार्य रूप से मानव तर्क का मशीन की तार्किक भाषा में अनुवाद किया, ओपन-सोर्स प्रोग्रामिंग भाषा लीन का उपयोग करके।
यह औपचारिकीकरण गणित में एआई की बढ़ती प्रगति में योगदान देता है, चाहे वह मानव शोधकर्ताओं की सहायता करे या नई तर्क उत्पन्न करे। इंपीरियल कॉलेज लंदन के गणितज्ञ केविन बज़ार्ड ने नेचर को दिए एक साक्षात्कार में टिप्पणी की कि दो साल पहले, ऐसी क्षमता को अभी भी कल्पना माना जाता था। शोधकर्ता बज़ार्ड 2024 से लीन में फर्माट के प्रमेय के औपचारिकीकरण पर काम कर रहे हैं।
लीन में गणितीय प्रदर्शन को औपचारिक रूप देने के लिए, सिस्टम को पूर्व अवधारणाओं, तर्कों और प्रमाणों को जानना आवश्यक है, क्योंकि गणितीय ज्ञान पहले से सत्यापित कथनों पर निर्मित होता है। अधिक जटिल प्रमाणों से निपटने के लिए, गणितज्ञों ने मैथलिब विकसित की, जो लीन में औपचारिकताओं की एक लाइब्रेरी है, जिसके समावेश विशेषज्ञों के मानव क्यूरेशन के अधीन होते हैं।
पहले, गणितीय प्रदर्शन की समीक्षा पूरी तरह से मानव विशेषज्ञों पर निर्भर करती थी जो तर्कों की तार्किक श्रृंखला को सत्यापित करने में वर्षों लगाते थे। हालांकि, कई प्रमाण कम दृश्यता वाले पत्रिकाओं में प्रकाशित होते हैं, जिससे उनकी पहुंच सीमित हो जाती है और उनकी वैधता अनिश्चित रहती है, जो उन गणित के क्षेत्रों में प्रगति को बाधित करता है जिन पर वे निर्भर करते हैं। कई गणितज्ञ उम्मीद करते हैं कि एआई द्वारा औपचारिकीकरण का मैथलिब और मानव जांच के साथ संयोजन वैज्ञानिक पत्रिका समीक्षकों के काम को अनुकूलित कर सकता है और गणितीय प्रगति को बढ़ावा दे सकता है।