Axiom का कहना है कि AI एजेंटों ने Lean में सीमित सरल समूहों के वर्गीकरण को औपचारिक रूप दिया

AI गणित कंपनी Axiom ने X पर सीमित सरल समूहों के वर्गीकरण का पूर्ण Lean स्वचालित-औपचारीकरण घोषित किया। कंपनी इसे “सममिति की आवर्त सारणी” कहती है। उसके अनुसार, मूल प्रमाण लगभग 15,000 पन्नों का था, जिसे कई पीढ़ियों के 100 से अधिक गणितज्ञों ने लिखा था। Axiom इसे इतिहास का सबसे बड़ा गणितीय प्रमाण बताती है जिसकी कंप्यूटर से पुष्टि की गई है।

Axiom के ओपन-सोर्स रिपॉज़िटरी के अनुसार, AI एजेंटों के झुंड ने 24 दिनों में Lean की लगभग 43.1 मिलियन पंक्तियाँ तैयार कीं। इस काम में 715 शोधपत्रों और पुस्तकों को शामिल किया गया और प्रकाशित रिकॉर्ड से 34 विचलनों को चिह्नित किया गया। AI समाचार अकाउंट TestingCatalog की एक पोस्ट के मुताबिक, एजेंटों ने सॉफ़्टवेयर टीमों की तरह काम बाँटा और Lean की जाँच की गति से भी तेज़ कोड लिखा।

ये आँकड़े Axiom के अपने दावे हैं; घोषणा में औपचारिकीकरण की कोई स्वतंत्र समीक्षा शामिल नहीं है। 28 अक्टूबर तक X पर पोस्ट को लगभग 6,200 लाइक्स मिले थे।