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