OpenAI kompaniyasi sunʼiy intellektning ichki modeli tomonidan ishlab chiqilgan yetti yuz yigirma ikki ta matematik hujjatni GitHub platformasida joylashtirdi. Ushbu qoʻlyozmalar uch yuz yetmish ikki natijalar oilasiga guruhlangan va matematika sohasining oʻn yetti xil yoʻnalishini qamrab oladi.
Taʼkidlangan isbotlarning baʼzilari Lean tilidan foydalanib formalizatsiya qilingan. Modelning yutuqlari orasida kombinatorial geometriya sohasidagi mashhur muammo boʻlgan Hadwiger-Nelson vazifasi uchun yangi isbot topilishi mavjud.
Model tekislikni bunday ranglash mumkin emasligini namoyish etdi, bunda bir-biridan aniq bitta birlik masofada joylashgan har qanday ikkita nuqta turli rangga ega boʻlishi kerak. Shu sababli, tekislikning xromatik soni endi olti yoki yetti boʻlishi mumkin. Ushbu isbot ham Lean tizimida formalizatsiya qilingan.