गणितज्ञ ने 24 घंटों के भीतर OpenAI के अनुमान की सफलता को खारिज किया: 'AI ने हर वाक्य साबित किया, लेकिन यह अब मूल अनुमान के बारे में नहीं है'

OpenAI ने दावा किया कि उसके अगली पीढ़ी के AI मॉडल ने दस विश्व-स्तरीय गणितीय समस्याओं को हल किया, जिसमें Connes rigidity conjecture को गलत साबित करना भी शामिल था। अगले दिन, एक मानव गणितज्ञ ने एक पेपर के साथ जवाब दिया जिसमें तर्क दिया गया कि AI का प्रतिउदाहरण अमान्य है। लेखिका, कैनसस विश्वविद्यालय के टोपोलॉजी फिजिक्स सेंटर की जे. एल. नीलसन ने OpenAI के 37,000 लाइनों के Lean 4 कोड को शुरू से अंत तक ट्रेस किया, प्रत्येक ऑब्जेक्ट को उसके गणितीय प्रोटोटाइप से मैप किया, और दो स्वतंत्र विफलता मार्गों की पहचान की। Connes rigidity conjecture कहता है कि यदि दो समूहों में एक ही संबद्ध बीजगणितीय संरचना है और वे दो अतिरिक्त शर्तों (ICC और Kazhdan की property (T)) को संतुष्ट करते हैं, तो समूह समरूपी होने चाहिए। OpenAI के मॉडल ने दो गैर-समरूपी समूह बनाए जो समान बीजगणित उत्पन्न करते हैं, जिनके प्रमाण दर्शाते हैं कि दोनों समूह ICC और property (T) को संतुष्ट करते हैं। नीलसन ने बताया कि AI-निर्मित समूहों में से एक वास्तव में अतिरिक्त शर्तों को संतुष्ट नहीं करता था, न तो ICC था और न ही उसमें property (T) थी। उन्होंने तीन संभावित कारण सूचीबद्ध किए: कोड में property (T) का प्रतिनिधित्व Kazhdan की मूल परिभाषा के अनुरूप नहीं था; प्रमाण केवल समूह के एक हिस्से के लिए था लेकिन पूरे समूह पर लागू किया गया था; या कोड में समूह वह नहीं है जो व्याख्यात्मक दस्तावेज़ में वर्णित है। नीलसन ने कोड की पंक्ति-दर-पंक्ति जाँच भी की, प्रत्येक गणितीय ऑब्जेक्ट के नाम और लाइन नंबर को एक क्रॉस-रेफरेंस तालिका में सूचीबद्ध किया। उन्होंने पाया कि ICC साबित करने के लिए उपयोग किए गए लेम्मा द्वैत परिवर्तन के बाद वस्तुओं पर लागू होते थे, न कि अपने केंद्रीय तत्वों के साथ मूल समूह पर, इसलिए वे सीधे महत्वपूर्ण तत्वों को कवर नहीं करते थे। उन्होंने अपने दो खंडनों को Lean कोड के रूप में लिखा और उन्हें Lean 4.32.2 के तहत संकलित किया। पेपर का अंतिम भाग व्यापक संदर्भ पर चर्चा करता है: Lean कर्नेल औपचारिक शुद्धता सुनिश्चित करता है, लेकिन यह नहीं कि कथन वास्तव में इच्छित निष्कर्ष साबित करता है या नहीं। टेरेंस ताओ को उद्धृत करते हुए, एक प्रमाण को सत्यापित करना औपचारिक कथन की जाँच करता है, न कि इरादे के साथ उसके संरेखण की, इसलिए मानव समीक्षा को प्रतिस्थापित नहीं किया जा सकता। पांच सामान्य Lean बेंचमार्क के पिछले ऑडिट में 4,833 मुद्दे मिले, जिनमें प्रतिउदाहरण, खाली प्रमेय और अविश्वसनीय स्वयंसिद्ध शामिल थे, ये सभी मशीन-सत्यापित थे, और बाद में मनुष्यों ने प्रतिउदाहरण बनाकर दिखाया कि साबित किए गए कथन गलत थे। नीलसन ने लिखा कि OpenAI का औपचारिकीकरण शायद हर निष्कर्ष को सही ढंग से स्थापित कर सकता है जिसका वह दावा करता है, लेकिन जो उसने स्थापित नहीं किया—और जिसे Lean कर्नेल जाँच नहीं सकता—वह यह है कि क्या ये निष्कर्ष मूल conjecture के शब्दों से संबंधित हैं। Connes rigidity conjecture अनसुलझा बना हुआ है।