गणितज्ञों ने प्रमेय सिद्ध करने में AI की हालिया प्रगति पर उत्साह और निराशा का मिला-जुला प्रतिकार किया है। कुछ AI उत्साही अब तर्क देते हैं कि आने वाली पीढ़ियों के लिए विरासत के रूप में सम्पूर्ण गणित को औपचारिक बनाने का समय आ गया है। लेखक, जो विशेषज्ञ औपचारिकरण करने वालों का एक समूह हैं और जिसमें Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash और Adam Topaz शामिल हैं, कहते हैं कि वे इस प्रस्ताव के प्रति सहानुभूति रखते हैं और AI की भूमिका को लेकर आशावादी हैं। फिर भी, वे हर चीज़ को यथाशीघ्र औपचारिक बनाने के आह्वानों से गहराई से चिंतित हैं।
यदि इसे अच्छे से किया जाए, तो एक बड़े पैमाने का, समन्वित औपचारिकरण प्रयास गणितीय अन्वेषण और खोज को काफी हद तक बढ़ा सकता है। लेखक चेतावनी देते हैं कि यदि इसे खराब तरीके से किया गया, तो यह सर्वोत्तम स्थिति में संसाधनों की बर्बादी होगा और सबसे बुरी स्थिति में स्थायी नुकसान पहुँचा सकता है। वे स्पष्ट करते हैं कि व्यक्त विचार उनके अपने हैं, न कि उन संस्थाओं के जिनसे वे जुड़े हैं, और उनके सहकर्मियों की AI-आधारित औपचारिकरण पर विचारों की एक विस्तृत श्रृंखला है।
लेखक हाल के उदाहरणों की ओर इशारा करते हैं। Maryna Viazovska के गोला-पैकिंग परिणामों को औपचारिक बनाने की एक परियोजना तब बाधित हो गई जब एक AI कंपनी ने उसे अपने हाथ में लेने का प्रयास किया। मूल टीम ने पाया कि AI-जनित कोड को साफ करना उसके मूल्य से अधिक झंझट भरा था, इसलिए उन्होंने उसे छोड़ दिया और AI की सहायता से कार्य को सही ढंग से फिर से बनाया। इसी तरह, जब Anthropic ने घोषणा की कि Claude ने 13 मिलियन लाइनों के कोड में फर्मा के अंतिम प्रमेय को औपचारिक रूप से सत्यापित कर दिया है, तो परिणाम प्रभावशाली था, पर उसका निरंतर मूल्य सीमित था, क्योंकि उस प्रमेय पर कभी गंभीर संदेह नहीं था।
मूल बात यह है कि एक औपचारिक कलाकृति तभी मूल्यवान है जब लोग उसका उपयोग करें। औपचारिकरण का महत्व शुद्धता से परे उन चीज़ों में है जो वे संभव बनाते हैं, जैसे सामान्यीकरणों की खोज, गणित की विभिन्न शाखाओं को जोड़ना, और अवधारणाओं को परिष्कृत करना। लेखकों का तर्क है कि इस प्रयास का मार्गदर्शन वास्तविक समझ से होना चाहिए, न कि सत्यापित कोड की कच्ची मात्रा से।
स्रोत: Hacker News · HeadlinesBriefing द्वारा सारांशित