Matematik isbot biror yakuniy xulosaga olib boradigan mantiqiy fikrlashlar ketma-ketligidir. Leonardo de Moura tomonidan 2013 yilda Rio de Janeirodan yaratilgan Lean dasturlash tili bu isbotlarni kamchiliklar yoki xatoliklarni aniqlash uchun tekshirish imkonini beradi.
Sentabrda Lean ChatGPT egasi boʻlgan OpenAI kompaniyasi Navier-Stokes matematik muammosiga yechim topganini eʼlon qilgandan soʻng bahs-munozaraning markaziy nuqtasi boʻldi. Bu muammo Mingilliy Muammolarining Yetti muammosidan biri boʻlib, uning yechimlari har biri uchun 1 million AQSh dollari miqdorda baholanadi. Ilmiy hamjamiyat bu namoyish asl masalani haqiqatan ham hal qilibmi deb bahslashmoqda, garchi u mantiqan mukammal ekanligi maʼlum boʻlsa va Lean buni taʼminlayotgan boʻlsa ham.
Bu imkoniyat 2023 va 2013 yillardagi kabi tasavvur qilib boʻlmaydigan edi. Muallif Microsoftda ishlayotganini aytadiki, u yerda nazariyalar isbotlovchilari dasturlar xatosiz ekanligini taʼminlash uchun ishlatilardi. Biroq, bu usul ichki ravishda dastur yaratishdan oʻn barobar qimmatroq edi, bu esa uni kriptografiya kabi muhim sohalarga cheklab qoʻyardi. Hech kim Fields medallari egasi boʻlgan Terence Tao kabi olimlarning bu tizimdan foydalanishini oldindan taxmin qila olmadi. Hozirda, agar kimdir Tao bilan bogʻlanib, guvaha qilishni daʼvo qilsa, uning javobi shunday boʻladi: «Avval Lean da tekshiring».
Koʻpgina matematiklar Lean mavjudligini bilmasdi va uda xatolari bormi yoki ishonchlimi kabi dolzarb savollarni koʻtarishmoqda. Navier-Stokes muammosining maxsus holatida, u Lean tilida yozilgan yuz minglab qatorlarni oʻz yaratgan tekshiruvchilar yordamida jamiyat aʼzolari tomonidan koʻrib chiqildi va u tasdiqlandi. Shunday qilib, ishonchsizlik inqilobi koʻproq axloqiy masalalarda, masalan, AI kompaniyalari ortiqcha suv isteʼmol qilishi yoki maʼlumotlarni oʻgʻirlashi kabi daʼvolarda yotadi. Garchi ular dolzarb mavzular boʻlsa-da, ular matematikaning taraqqiyotini toʻxtata olmaydi.
Turli xil reaksiyalar mavjud: baʼzilari hayajonni namoyish etadi, boshqalari eskirib qolishdan qoʻrqadi va baʼzilari sunʼiy intellekt matematikaning yoʻq boʻlishiga sabab boʻlishiga ishonadi. Hayotdagi eng buyuk matematiklardan biri hisoblangan Peter Scholze AI dan foydalanmasdan oʻlishi kerakligini eʼlon qildi. Boshqa tomondan, Kevin Buzzard Lean da Fermatning Oxirgi teoremasini rasmiylashtirish uchun besh yillik loyiha rejalashtirgan edi. Aprelda, AI yordam beradimi deb soʻralganda, u kulib yubordi; bir necha oy oʻtgach, u bu ishni atigi 11 kunda bajardi. Muallif koʻplari «koʻrishgacha qaygʻu» davrida ekanligini xulosa qiladi, bu hisob-kitoblarni miyada bajaradiganlarning kalkulyator paydo boʻlishiga nisbatan reaksiyasiga oʻxshaydi, chunki kalkulyator dastlabki qarshilikka qaramay, insoniyatga foyda keltirdi. U AI ga qarshi chiqmaslikni oʻrgandi.