Claude 11 kunda Fermat teoremasini kompyuter tekshiruvli isbotladi
Anthropic'ning Claude modeli Fermatning So'nggi Teoremasining birinchi to'liq kompyuter tekshiruvli isbotini yozdi: 11 kun, 13 million qator Lean kodi, 29 500 teorema. Bu nima uchun muhim va nima uchun emas.
1637-yilda fransuz matematigi Pyer de Ferma o’z daftarining chetiga bitta yozib qoldirdi. Yoniga «isbotim juda ajoyib, lekin joy sig’maydi» deb yozib qo’ydi.
358 yil davomida hech kim buni isbotlay olmadi. 1995-yilda britaniyalik Endryu Uayls yagona to’liq isbotni e’lon qildi — 129 sahifa. Tekshirish oylab oldi.
2026-yil 4-sentabrda Anthropic shuni e’lon qildi: Claude bu isbotning birinchi to’liq kompyuter tekshiruvli versiyasini yozdi. 11 kun ichida, asosan mustaqil ishlab.
Raqamlar
- 11 kun — Claude’ning ishlash davomiyligi, inson aralashuvi minimal bo’lgan
- 13 million qator Lean dasturlash tilida yozilgan kod
- 29 500 oraliq teorema isbotlangan — bu Lean’ning asosiy kutubxonasi Mathlib’dan 5 baravar ko’p
Tianyi Peng — Anthropic tadqiqotchisi, Kolumbiya universitetidagi guruhi AI formalizatsiya vositalarini quradi — Claude’ga «Fermat teoremasini formalizatsiya qilishda progressiya qila oladimi?» degan savol bilan murojaat qildi. Natija kutgandan uzoqroqka chiqdi.
«Kompyuter tekshiruvli» degani nima
Bu yerda muhim noziklik bor. Claude yangi matematika ochmadi. U Uaylsning mavjud isbotini boshqa formatga — Lean tiliga — o’girdi.
Lean — bu «tekshiruvchi» dasturlash tili. Unda yozilgan isbotni kompyuter qator-bo-qator, hech qanday taxminsisiz tekshiradi. Kalkulyator hisobni tekshirgani kabi — faqat bu hisob emas, mantiqiy zanjir. Agar bitta qadamda yolg’on bo’lsa, butun isbot yiqiladi.
Ya’ni: matematiklar 30 yildan beri «ishonamiz» degan isbot endi matematik aksiomalardan boshqa hech narsaga tayanmaydi. Inson tekshiruvchining charchashi, e’tiborsizligi, roziligi — zararli emas, chunki tekshiruvni mashina qiladi.
Nima uchun bu muhim
Buzzard — London Imperial kollejida yillar davomida aynan shu ishni o’zi qilmoqchi bo’lgan taniqli matematik — Anthropic’ning natijasini ko’rib shunday dedi:
«Ajoyib avtoformalizatsiya yutug’i… Bu AI avtoformalizatsiya artefaktlari endi ularga qurilish qilish uchun yetarlicha mustahkam ekanini ko’rsatadi.»
Asosiy saboq: insoniyatning eng murakkab matematik isbotlarini kompyuter tiliga o’girish — yillar emas, kunlar oladigan ishga aylanmoqda. AI ko’proq teorema isbotlagan sari, ularni tekshirish nazariyasi ham shunchalik osonlashadi — yangi natijani kutish yillar emas, daqiqalar oladi.
Nima uchun emas
Buzzard o’zi ham buni yozdi: «Matematik jihatdan bu ish bizga asosan hech narsa bermaydi. Isbot to’g’ri ekaniga 99,9% ishongan edim.» FLT allaqachon 30 yildan beri sinchiklab tekshirilgan — formalizatsiya yangi bilim bermadi, yangi kafolat berdi.
Ikkinchi cheklov: 13 million qator kodni hech bir inson qator-bo-qator o’qimagan. Kompyuter tekshiruvi Lean’ning o’zi to’g’ri ishlayotganiga tayanadi — bu ham texnik dizayn masalasi, mutlaq kafolat emas.
O’zbekiston uchun
Bu yangilik faqat matematiklar uchun emas. U «AI nima qila oladi va nima qila olmaydi» degan savolga yana bitta aniq javob: halol, tekshiriladigan ish — AI’ning eng kuchli tomoni. Inson 30 yil ishonga qurilgan narsani 11 kunga mustahkam qila oladi.
Fermat o’z daftarining chetida yozib qoldirgan so’z 389 yildan keyin — endi kompyuter ham tan olgan holda — o’z yakuniga yetdi.
Manba: Anthropic rasmiy e’loni anthropic.com/research/formalizing-fermats-last-theorem, 2026-09-04. Isbot kodi: github.com/anthropics/fermats-last-theorem. Buzzard sharhi: Xena Project blogi.