Chombo cha habari za teknolojia Gigazine kilichapisha jana (Agosti 3) makala ikiripoti kwamba uthibitisho rasmi wa Lean uliokamilishwa kwa msaada wa AI na kudai kukanusha dhana ya Collatz umethibitishwa kuwa batili.
Kumbuka: Dhana ya Collatz (pia huitwa dhana ya uradibishaji wa usawa/3n+1) ilipendekezwa na mwanahisabati Mjerumani Lothar Collatz mwaka 1937. Ni tatizo la kihisabati lenye maelezo rahisi sana lakini ambalo bado halijatatuliwa, likidai kwamba kila nambari kamili chanya, baada ya kurudiwa kwa kanuni maalum, hatimaye itarudi kwenye 1.
Kanuni ya kukokotoa ni hii kwa nambari yoyote kamili chanya n:
Ikiwa n ni nambari shufwa, igawanye kwa 2 (n ÷ 2).
Ikiwa n ni nambari witiri, izidishe kwa 3 kisha ongeza 1 (3n + 1).
Baada ya kupata nambari mpya, rudia hatua hizo hadi matokeo yawe 1.
Kwa mfano, kwa nambari 6:
6 ni shufwa, ikigawanywa kwa 2 inakuwa 3
3 ni witiri, ikizidishwa kwa 3 na kuongezwa 1 inakuwa 10
10 ni shufwa, ikigawanywa kwa 2 inakuwa 5
5 ni witiri, ikizidishwa kwa 3 na kuongezwa 1 inakuwa 16
16 ikigawanywa kwa 2 mfululizo inakuwa 8, 4, 2, 1
Njia ya mwisho ni: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.
Mtaalamu wa uthibitishaji rasmi Ramana Kumar alichapisha mradi kwenye GitHub tarehe 25 Julai, mwanzoni akidai kwamba alikuwa amekanusha dhana ya Collatz kwa msaada wa AI. Mradi huo haukutoa nambari kamili maalum ya kupinga dhana hiyo, bali ulithibitisha katika Lean (mfumo msaidizi wa uthibitishaji wa teoremi) kwamba “kuna nambari isiyoweza kufikia 1”.
Lean ni mfumo msaidizi wa uthibitishaji wa teoremi unaowawezesha watumiaji kuandika fomula za kihisabati na mantiki kama programu, kisha kompyuta kuthibitisha usahihi wa uthibitisho. Msimbo wa Lean unaoandikwa na mtumiaji hubadilisha kauli za kihisabati na uthibitisho kuwa programu inayoweza kukaguliwa, na kernel huthibitisha ulinganifu wa aina na mantiki.
Hata hivyo, alipokagua baadaye maudhui ya kukanusha, aligundua kwamba mbinu hiyo ingeweza hata kuifanya Lean ikubali bila masharti “False” (inayowakilisha kauli ya uongo). Kwa hiyo, msimbo husika kwa sasa hauwezi kukanusha dhana ya Collatz.
Mtafiti wa uthibitishaji rasmi Kiran Gopinathan aliufupisha tatizo kuwa msimbo mdogo wa kuzalisha upya na kuliripoti kwa timu ya watengenezaji wa Lean tarehe 28 Julai 2026.
Kasoro hiyo ilikuwa katika sehemu ya kernel inayoshughulikia “aina za urudiaji zilizopachikwa”, na wakati mwingine ilisababisha kupuuzwa kwa “vigezo vya aina vizuka” (yaani vigezo visivyojitokeza moja kwa moja katika vipengele vya muundo wa data), hivyo vigezo ambavyo vilipaswa kutambuliwa kuwa na hitilafu viliweza kupita ukaguzi. Msanidi wa Lean Leonardo de Moura alisema tatizo lilitokana na utekelezaji wa kernel kutokamilisha ukaguzi uliostahili.
Timu ya Lean iliunda ombi la kuvuta la kurekebisha tatizo hilo takriban saa 1 baada ya kupokea ripoti, na tarehe 28 Julai ikatoa toleo la Lean 4.32.2, lililorekebisha tatizo hilo.