एक गणितीय प्रमाण तर्क की एक श्रृंखला होती है जो एक निश्चित निष्कर्ष पर ले जाती है। लीन, एक प्रोग्रामिंग भाषा जिसे 2013 में रियो डी जनेरियो के लियोनार्डो डी मौरा द्वारा बनाया गया था, इन प्रमाणों को दोष या त्रुटियों की पहचान करने के लिए सत्यापित करने की अनुमति देता है।
सितंबर में, लीन विवाद का केंद्र बन गया जब ओपनएआई, चैटजीपीटी की मूल कंपनी, ने नेवियर-स्टोक्स की गणितीय समस्या के लिए एक समाधान की घोषणा की, जो मिलेनियम समस्याओं के सात में से एक है, जिसके समाधानों का मूल्यांकन प्रत्येक $1 मिलियन में किया जाता है। वैज्ञानिक समुदाय इस बात पर बहस कर रहा है कि क्या यह प्रदर्शन वास्तव में मूल मुद्दे को संबोधित करता है, हालांकि यह एक तथ्य है कि यह तार्किक रूप से सही है, जैसा कि लीन सुनिश्चित करता है।
यह संभावना 2023 और 2013 दोनों में अकल्पनीय थी। लेखक बताते हैं कि वह माइक्रोसॉफ्ट में काम करते थे, जहां सॉफ्टवेयर में खामियों से मुक्त होने के लिए प्रमेय सिद्ध करने वालों को नियुक्त किया जाता था। हालांकि, यह तरीका आंतरिक रूप से कार्यक्रम विकसित करने की तुलना में दस गुना अधिक महंगा था, जिससे इसका उपयोग क्रिप्टोग्राफी जैसे महत्वपूर्ण क्षेत्रों तक सीमित हो गया था। किसी ने अनुमान नहीं लगाया था कि फील्ड्स पदक विजेता, जैसे टेरेन्स टाओ, इस प्रणाली का उपयोग करेंगे। वर्तमान में, जब कोई टाओ से संपर्क करके किसी परिकल्पना को सिद्ध करने का दावा करता है, तो उनका जवाब होता है: 'पहले लीन में जांच करें'।
कई गणितज्ञ लीन के अस्तित्व से अनजान थे और प्रासंगिक प्रश्न उठाते हैं, जैसे कि क्या इसमें कोई खामियां हैं या क्या इस पर भरोसा किया जा सकता है। नेवियर-स्टोक्स के विशिष्ट मामले में, जिसमें लीन में लिखे गए लाखों लाइनें हैं, समुदाय के सदस्यों ने अपने स्वयं के बनाए गए सत्यापनकर्ताओं का उपयोग करके प्रमाण की जांच की, और इसे मंजूरी मिल गई। इस प्रकार, विश्वास का संकट अधिक नैतिक मुद्दों में निहित है, जैसे कि एआई कंपनियों द्वारा अत्यधिक पानी का उपभोग करना या डेटा चुराना। हालांकि ये प्रासंगिक विषय हैं, वे गणित की प्रगति को नहीं रोक सकते।
विभिन्न प्रतिक्रियाएं हैं: कुछ उत्साह दिखाते हैं, अन्य अप्रासंगिक होने के डर से महसूस करते हैं, और कुछ मानते हैं कि आर्टिफिशियल इंटेलिजेंस गणित को नष्ट कर देगा। पीटर शोलज़, जिन्हें जीवित सबसे महान गणितज्ञों में से एक माना जाता है, ने घोषणा की कि वह एआई का उपयोग किए बिना मर जाएंगे। दूसरी ओर, केविन बज़र्ड ने लीन में फर्माट के अंतिम प्रमेय को औपचारिक रूप देने के लिए पांच साल की परियोजना की योजना बनाई थी। अप्रैल में, जब उनसे पूछा गया कि क्या एआई मदद करेगा, तो वह हँसे; महीनों बाद, इसने केवल 11 दिनों में काम पूरा कर लिया। लेखक निष्कर्ष निकालते हैं कि कई लोग एक 'शोक' का अनुभव कर रहे हैं, उन लोगों की प्रतिक्रिया की तुलना कैलकुलेटर के आने पर मानसिक गणना करने वालों से करते हैं, जिसने प्रारंभिक प्रतिरोध के बावजूद मानवता को लाभ पहुंचाया। उन्होंने सीखा कि एआई को चुनौती न दें।