Texnologiya nashri Gigazine kecha (3-avgust) blog postini e’lon qilib, AI yordamida tayyorlangan va Kollats farazini rad etishni da’vo qilgan Lean formal isboti haqiqiy emas deb topilgani haqida xabar berdi.
Eslatma: Kollats farazi (shuningdek, juft-toqlikni normallashtirish farazi yoki 3n+1 farazi deb ham ataladi) nemis matematigi Lothar Collatz tomonidan 1937 yilda ilgari surilgan. Bu ifodalanishi nihoyatda sodda, ammo hozirgacha yechilmagan matematik muammo bo‘lib, istalgan musbat butun son muayyan qoidalar asosida qayta-qayta o‘zgartirilgach, oxir-oqibat albatta 1 ga qaytishini ta’kidlaydi.
Hisoblash qoidasi istalgan musbat butun n soni uchun quyidagicha:
Agar n juft bo‘lsa, uni 2 ga bo‘ling (n ÷ 2).
Agar n toq bo‘lsa, uni 3 ga ko‘paytirib, 1 qo‘shing (3n + 1).
Yangi son hosil bo‘lgach, natija 1 ga aylanguncha yuqoridagi qadamlarni takrorlang.
6 sonini misol qilib olaylik:
6 juft son, 2 ga bo‘lsak 3 hosil bo‘ladi
3 toq son, 3 ga ko‘paytirib, 1 qo‘shsak 10 hosil bo‘ladi
10 juft son, 2 ga bo‘lsak 5 hosil bo‘ladi
5 toq son, 3 ga ko‘paytirib, 1 qo‘shsak 16 hosil bo‘ladi
16 ni ketma-ket 2 ga bo‘lsak 8, 4, 2, 1 hosil bo‘ladi
Yakuniy yo‘l: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.
Formal verifikatsiya mutaxassisi Ramana Kumar 25-iyul kuni GitHub’da loyiha e’lon qilib, dastlab AI yordamida Kollats farazini rad etganini aytdi. Loyihada muayyan qarshi misol bo‘ladigan butun son keltirilmagan, faqat Lean’da (teoremalarni isbotlashga yordam beruvchi tizim) “1 ga yetib bormaydigan son mavjud” degan fikr isbotlangan.
Lean matematik formulalar va mantiqni dastur shaklida yozish hamda isbotning to‘g‘riligini kompyuter orqali tekshirish imkonini beruvchi teorema isbotlash yordamchi tizimidir. Foydalanuvchi yozgan Lean kodi matematik mulohaza va isbotni tekshiriladigan dasturga aylantiradi, yadro esa turlar va mantiqiy izchillikni tekshiradi.
Biroq u keyinchalik rad etuvchi mazmunni ko‘rib chiqayotganda, tegishli usul Lean’ni “False”ni (yolg‘on mulohazani ifodalovchi qiymat) hech qanday shartsiz qabul qilishga ham majbur qilishi mumkinligini aniqladi. Shu sababli tegishli kod hozircha Kollats farazini rad eta olmaydi.
Formal verifikatsiya tadqiqotchisi Kiran Gopinathan muammoni kichik reproduksiya kodiga qisqartirdi va 2026-yil 28-iyul kuni bu haqda Lean ishlab chiquvchilar jamoasiga xabar berdi.
Zaiflik yadroda “ichma-ich induktiv turlar”ni qayta ishlash qismida joylashgan bo‘lib, ba’zan “arvoh tur parametrlari”ni (ya’ni ma’lumotlar strukturasi komponentlarida bevosita ko‘rinmaydigan parametrlarni) e’tibordan chetda qoldirgan. Natijada aslida xato deb topilishi kerak bo‘lgan parametrlar tekshiruvdan o‘tib ketgan. Lean dasturchisi Leonardo de Moura muammo yadro implementatsiyasida zarur tekshiruvlar to‘liq amalga oshirilmagani bilan bog‘liqligini bildirdi.
Lean jamoasi xabarni olganidan taxminan 1 soat o‘tib tuzatish pull-requestini yaratdi va 28-iyul kuni Lean 4.32.2 versiyasini e’lon qilib, muammoni bartaraf etdi.