1637-yilda matematik Pierre de Fermat $x^n + y^n = z^n$ tenglamasi haqida bayonot berdi, bunda $x, y, z$ va $n$ musbat butun sonlardir. Fermat bu tenglamaning darajasi $n$ ikki dan katta boʻlsa, toʻgʻri yechimi mavjud emasligini taʼkidladi.
Bu shuni anglatadiki, $x, y$ va $z$ uchun bunday qiymatlar kombinatsiyasi yoʻqki, u bayonotni rost qiladi; Fermatning fikricha, $x^n$ ning $y^n$ ga qoʻshilishi hech qachon $z^n$ natijasini bermaydi. $n$ ning 2 dan katta boʻlishi zaruriyati Pisagor teoremasi ($x^2 + y^2 = z^2$) bilan solishtirilishi mumkin, u $3^2 + 4^2 = 5^2$ misolida koʻrsatilganidek, toʻgʻri boʻlib, Fermatning inkor etilishi $n=2$ boʻlganda qoʻllanilmasligini isbotlaydi.
Fermat yechimlarning imkonsizligi $n=3, n=4$ va boshqa kattaroq qiymatlar uchun davom etishini taxmin qildi, ammo u oʻz xayolidagi isbotni hech qachon yozib olmadi. Bu tushuncha Fermatning Oxirgi teoremasi deb nomlanadi. Kimdir Fermatning toʻgʻriligini isbotlash uchun 357 yil kutdi, Andrew Wiles 1994-yilda isbotni yakunlagan boʻlib, bu XX asrining ilmiy yutuqlari hisoblanadi. Ushbu gʻalaba uchun Wiles 2016-yilda Abel mukofotini oldi.
Yaqinda sunʼiy intellekt modeli Claude prototipi ushbu isbotni 13 million qatordan iborat tekshiriladigan kodga aylantirdi. Claude ishlab chiquvchisi Anthropic bu eʼlonni sentyabrning 4-ida eʼlon qildi. Sunʼiy intellekt loyihani yakunlash uchun atigi 11 kun sarfladi, shu bilan birga, odamlar xuddi shu ishni bajarish uchun taxminan 10 yil sarflashi kutilmoqda.
Muhim jihat shundaki, Claude muammoni hal qilmagan, balki uning isbotini rasmiylashtirdi. U aslida tabiiy tilda (soʻzlar) yozilgan isbotni kompyuter tekshirish mumkin boʻlgan rasmiy isbotga aylantirdi, mohiyatiga koʻra, inson argumentini mashinalarning mantiqiy tiliga tarjima qildi, bu jarayonda ochiq kodli Lean dasturlash tili ishlatildi.
Bu rasmiylashtirish matematikada AI ning tobora ortib borayotgan taraqqiyotlari mahsuliga hissa qoʻshmoqda, ham inson tadqiqotchilarga yordam berish orqali, ham yangi fikrlashlarni yaratish orqali. Londondagi Imperial College matematik Kevin Buzzard Nature jurnaliga bergan intervyusida, ikkita yil oldin bunday qobiliyat hali fiksiya deb hisoblanganini taʼkidladi. Tadqiqotchi Buzzard 2024-yildan beri Fermat teoremasini Lean tilida rasmiylashtirish ustida ishlamoqda.
Lean tilida matematik isbotni rasmiylashtirish uchun tizim oldingi tushunchalar, argumentlar va isbotlarni bilishi kerak, chunki matematik bilim allaqachon tasdiqlangan bayonotlar asosida quriladi. Kengayib borayotgan murakkab isbotlar bilan ishlash uchun matematiklar Lean dagi rasmiylashtirishlar kutubxonasi boʻlgan Mathlibni ishlab chiqdilar, uning qoʻshimchalari inson mutaxassislari tomonidan nazorat qilinadi.
Avval matematik isbotlarni koʻrib chiqish faqatgina inson mutaxassislar tomonidan argumentlarning mantiqiy ketma-ketligini tekshirish uchun yillar sarflashga bogʻliq edi. Biroq, koʻplab isbotlar kamroq koʻrinadigan jurnallarda nashr etiladi, bu esa ularning doirasini cheklaydi va ularning haqiqiyligini noaniq qoldiradi, bu esa ularga bogʻliq baʼzi matematika sohalaridagi taraqqiyotni toʻxtatadi. Koʻplab matematiklar AI orqali rasmiylashtirishni Mathlib va inson tekshiruvi bilan birlashtirishning ilmiy jurnallar muhokimachilarining ishini optimallashtirishi va matematik taraqqiyotni tezlashtirishi mumkinligiga umid qilishmoqda.