Qadimgi Yunonistonda Evklid bir nechta oddiy aksiomalardan foydalanib, mantiqiy deduksiya orqali yangi matematik haqiqatlarni kashf etdi. Ammo bu dastlabki isbotlar ba'zan yashirin taxminlar yoki noto'g'ri intuitsiyalarga tayanar edi. Bugun matematiklar eng ulkan formalizatsiya loyihasini amalga oshirmoqda: barcha matematikani Lean deb nomlangan kompyuter dasturida qayta yozish.

Minglar Yillik Muammo

Matematik isbot — bu nafaqat to'g'ri javob topish, balki har bir qadamning mantiqan bir-biridan kelib chiqishini ko'rsatishdir. Ammo tarix davomida hatto buyuk matematiklar ham isbotlarida yashirin bo'shliqlar qoldirib ketgan.

XVII asrda Isaak Nyuton va Gotfrid Leybnits mustaqil ravishda matematikaning eng qudratli qurollaridan birini — infinitezimal hisobni (calculus) kashf etdilar. Bu usul funksiyaning qanday tezlikda o'zgarishini tushunish imkonini berdi. Ammo ularning isbotlari zamonaviy standartlar bo'yicha unchalik rasmiy emas edi.

Hisob cheksizlik va cheksiz kichik miqdorlar (infinitezimallar) tushunchalariga asoslanadi. Nyuton va Leybnits bu tushunchalarni noaniq geometrik atamalar bilan ta'riflashdi. Noto'g'ri ishlatilganda formulalar bema'ni natijalarga — nolga bo'lish kabi — olib kelishi mumkin edi.

150 yil davomida bu muammo hech kimga xalaqit bermadi. Olimlar faqat hisob qachon to'g'ri ishlatilishini va qachon ishlatilmasligini bilishni o'rgandilar. Ammo XIX asr boshida matematiklar o'z intuitsiyasiga zid hodisalar — cheksiz yig'indilar va g'alati, notekis egri chiziqlar — bilan to'qnasha boshladilar.

"Intuitsiya shubhali. Intuitsiya sizni noto'g'ri yo'lga boshlashi mumkin — degan his paydo bo'ldi."

— Alma Steingart, Kolumbiya universiteti tarixchisi

Qat'iylikning Tug'ilishi

Nils Abel, Ogüsten-Lui Koshi va Karl Veyershtrass kabi buyuk matematiklar asosiy ta'riflariga qaytishga majbur bo'ldi. Funksiya nima? Funksiyaning uzluksizligi nima? Cheksiz ko'p ob'ektni qo'shganingizda nima bo'ladi?

Ular bu savollarga rasmiy ta'riflar topdilar. Masalan, Veyershtrass bugungi kunda talabalarga o'rgatiladigan limitning aniq ta'rifini kiritdi. Bu yangi ta'riflar matematiklarga funksiyalarni ilgari hech qachon bo'lmagan darajada chuqur o'rganish imkonini berdi — va oxir-oqibat analiz sohasini vujudga keltirdi.

Bugun analiz matematikaning eng muhim sohalaridan biri hisoblanadi. U matematiklarga suyuqlik oqimi va elektr tokidan tortib uzoq yulduzlarning kimyoviy tarkibigacha hamma narsani tushunish imkonini beradi. Bundan tashqari, hisob formallashtirish to'plamlar nazariyasining tug'ilishiga ham olib keldi — zamonaviy matematikaning asosini tashkil etuvchi qoidalar.

Ammo ba'zi olimlar bu yangi qat'iylik to'lqiniga ehtiyotkorlik bilan munosabatda bo'ldilar.

"Tahlil qat'iylik va umumiylikka erishdi, ammo nafosatini va soddaligini yo'qotdi va intuitsiyadan uzoqlashdi. Ko'plab matematiklar bu tendensiyadan afsuslandilar."

— Tarixchi Jesper Lützen

Bourbaki: Qat'iylikni Haddan Oshirish

1930-yillar o'rtasida Fransiyada matematika o'nlab yillar davomida inqirozda edi. Birinchi Jahon Urushi mamlakat uchun istiqbolli talabalar va tadqiqotchilar avlodini yo'q qildi. Universitetlar matematikani muvofiqlashtirilmagan, tarqoq yo'llar bilan, eski materiallar asosida o'rgatardi.

Bir nechta yosh matematik Bourbaki deb nomlangan maxfiy jamiyat tuzdi. Ular frantsuz o'quv dasturini zamonaviy davrga moslashtirish uchun yangi, yaxlitroq darslik yozish bilan boshladilar. Tez orada esa ularning ambitsiyalari ancha ulkanroq bo'lib qoldi. Bugun Bourbaki (a'zolari sir saqlanadi) matematikaning barcha tasavvur qilinadigan sohalarini qamrab oladigan 40 dan ortiq jild nashr etdi.

Bourbaki falsafasi tezda tarqaldi va deyarli hamma joyda matematikaga ta'sir qildi. Fan yanada mustahkam bo'ldi, ammo tobora mavhum va qiyin bo'lib qoldi.

Ammo Bourbakining loyihasi kutilmagan oqibatlarga ham olib keldi. Ularning lug'ati va uslubi har turdagi matematikaga mos kelmadi. Masalan, kombinatorika (sanash fani) va graflar nazariyasi (tarmoqlar fani) ko'pincha juda aniq va vizual bo'ladi. Bourbakining ta'siri kuchli bo'lgan joylarda — AQSh va Yevropaning ko'p qismida — bu sohalar chetga surildi.

"Graflar nazariyasi topologiyaning mahallasi edi. Bu atmosfera faqat yaqinda o'zgardi. Juda yaqinda."

— Béla Bollobás, Kembrij universiteti

"Men bitta rejim hukmron bo'lgan hech qanday matematikani xohlamayman. Matematikaning saqlanishga loyiq madaniy tarixi bor."

— Aravind Asok, Janubiy Kaliforniya universiteti

Lean: Kompyuter Inqilobi

Bourbaki, Koshi va Veyershtrass ning barcha sa'y-harakatlariga qaramasdan, haqiqatan ham rasmiy isbotlar har doim nazariya ob'ektlari bo'lib qoldi, amaliyot emas. Endi ba'zi matematiklar kompyuterlar buni o'zgartira olishiga umid qilishmoqda.

1960-yillardan beri tadqiqotchilar isbot yordamchilari deb nomlangan kompyuter dasturlarini ishlab chiqmoqda. Isbot yordamchisidan foydalanib, matematik isbotning har bir qatorini (har bir ta'rifni ham) kompyuter tushunadigan tilda yozadi, so'ngra dastur mantiqni tekshiradi. Agar bitta qadam oldingi qadamdan kelib chiqmasa, dastur isbotni to'g'ri deb hisoblamaydi.

Hozirda matematiklar Lean deb nomlangan isbot yordamchisidan foydalanib barcha matematikani formalizatsiya qilishga umid qilmoqda. Ular hozirgacha 120,000 dan ortiq ta'riflar kutubxonasini yaratdi va 250,000 dan ortiq teoremani tasdiqladi. Bir nechta matematik bu ma'lumotlar bazasini yangilab turadi. Ular asosan asosiy investor Aleks Gerkodan 10 million dollardan ortiq moliyalashtirish olishdi.

"Har safar kosmik kema qurishda har bir muhandis har bir komponentni — temir rudani qazib olishdan, uni eritishdan, loyihalashdan — tushunishiga to'g'ri keladi deb tasavvur qiling. Endi bu rasmiy tizimlar bilan birinchi marta siz kimningdir qismini tayyor holda sotib olishingiz mumkin."

— Aleks Kontorovich, Rutgers universiteti

Lean Qanday Ishlaydi?

Lean isbotni ko'plab qismlarga bo'lib tashlaydi — ularning har biri alohida ko'rib chiqilishi, mustaqil ravishda tekshirilishi va boshqa isbotlarda qayta ishlatilishi mumkin.

2019-yilda matematik Peter Sholze qo'lda yangi teorema isbotini yozdi. Ammo isbot juda murakkab edi va u to'g'riligini aniqlashga qiynaldi. Shuning uchun 2020-yil oxirida Yohan Kommelin va Adam Topaz boshchiligidagi matematiklar guruhi isbotni Lean dasturida formalizatsiya qilishga kirishdi. Bir necha oy o'tgach, ular isbotning to'g'riligini tasdiqladi. Va bu jarayonda ular isbotning yanada soddalashtiriligini topdilar va Sholzening dastlabki g'oyalarini yanada takomillashtirdi.

"Bu sizi matematikada to'g'ri tarzda fikrlashga majbur qiladi. Bu sizni san'atkor bo'lishga majbur qiladi."

— Kevin Buzzard, Imperial College London

Buzzard hozirda Lean yordamida matematikaning eng mashhur natijalaridan biri — Fermat's Last Theorem isbotini formalizatsiya qilish ustida ishlayapti.

"Men bu argumentni go'zallik asari bo'lishini xohlayman. U tomog'ingizdan osonlikcha o'tishini xohlayman."

— Kevin Buzzard

Lean va Sun'iy Intellekt

Bundan tashqari, Lean ni hozir ishlab chiqish sun'iy intellekt kattaroq rol o'ynaydigan kelajakka yaxshi sarmoya bo'lishi mumkin. Matematiklar AI yordamida norasmiy isbotlar yozishga urinayotganida, ularning to'g'riligini Lean kabi dasturlar yordamida tekshirish yanada muhimroq bo'ladi.

AI allaqachon Lean isbotlarini yanada samarali yozishga yordam bermoqda. Kelgusida AI va Lean birgalikda ishlashi matematikani tubdan o'zgartirishi mumkin — yangi teoremalarni kashf etish va isbotlashda insoniyatga yordamchi bo'lishi mumkin.

Xavflar Mavjud

Ammo Lean keng qabul qilinishi bilan bog'liq xavflar ham mavjud. Lean ichida tushunchaviy, metodologik yoki mafkuraviy xilma-xillik uchun kam joy bor.

Leandagi har bir yangi isbot faqat allaqachon tasdiqlangan va kutubxonada saqlangan rasmiy ta'riflar va teoremalardan foydalanishi mumkin. Bu ta'riflar va isbotlar bir-biriga muammosiz mos kelishi kerakligini anglatadi. Bu esa muammoli bo'lishi mumkin.

"Matematika — bu qat'iy va cheklangan va formalizatsiya qilingan korxona emas. Bu harakatlanuvchi, o'zgaruvchan maxluq va uning shartlari doimo o'zgarib turadi."

— Stefani Dik, Saymon Freyzer universiteti

Bundan tashqari, Lean tili va kutubxonasiga kiritilgan ta'riflarning tanlovi matematikaning ba'zi sohalariga boshqalardan ko'ra ko'proq mos keladi. Ular son nazariyasi va algebraik geometriya uchun yaxshi mos keladi. Ammo graflar nazariyasi va kategoriyalar nazariyasi uchun emas.

Riehl Lean ning Bourbaki kabi matematikaning ayrim turlarini siqib chiqarishi, matematiklar o'zlari bilmagan holda faqat osonroq formalizatsiya qilinishi mumkin bo'lgan tushunchalarni rivojlantirishga e'tibor qaratishi mumkinligidan tashvishlanadi.

"Bu aslida e'tibor va intuitsiyani matematik muammo sohasidan bu tizimning xatti-harakatiga qarata o'zgartiradi."

— Stefani Dik

Muvozanat Izlash

Asrlar davomida matematiklar har bir isbot qatorini tekshirib bo'ladimi yoki yo'qmi degan savolga e'tibor qaratib, katta qat'iylikka intilishdi. Ammo bu har doim shunday bo'lmagan.

1600-yillarda Dekart uchun qat'iylik biror g'oyani xayolda ushlab turish va uni nima uchun to'g'ri ekanligini intuitiv tushunish qobiliyatini anglatardi. Zamonaviy isbotlar yanada nafisroq, ammo miyaning ularni anglashi uchun yanada ko'proq harakatlanishi kerak.

"Isbotning matematikaning markazi bo'lishiga hech qanday shubha yo'q. Ammo u matematikaning belgilovchi xususiyati bo'lishi kerakmi yoki yo'qmi — bu savol bo'lishi kerak."

— Akshay Venkatesh, Ilg'or tadqiqotlar instituti

Lean formalizatsiyasi isbotni ustuvor qilish tendentsiyasini davom ettiradi. Ammo tarix shuni ko'rsatadiki, matematika o'z-o'zini tuzatish qobiliyatiga ega. Formalizatsiyaning bu yangi to'lqinining kelajagi hali biz tasavvur qilmagan narsa bo'lishi mumkin.

Eng muhimi — ijodkorlik va qat'iylik o'rtasidagi muvozanatni saqlab qolish. Yangi matematikani kashf etish uchun intuitsiya va tajriba kerak. Ammo bu kashfiyotlarning to'g'riligini ta'minlash uchun qat'iylik zarur. Lean — bu muvozanatni yangi darajaga olib chiqishning vositasi bo'lishi mumkin.

Manba: Quanta Magazine — "In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?", muallif: Leila Sloman (25-mart, 2026). Maqola o'zbek tiliga moslashtirilgan va qayta ishlangan.