Umthombo wezindaba zobuchwepheshe i-Gigazine ushicilele umbhalo izolo (Agasti 3), ubika ukuthi ubufakazi obusemthethweni ku-Lean, obuqedwe ngosizo lwe-AI futhi obabuthi buphikisa umbono ka-Collatz, buqinisekiswe njengobungasebenzi.
Qaphela: Umbono ka-Collatz (owaziwa nangokuthi umbono wokujwayeleka kokulingana nokungalingani / umbono we-3n+1) waphakanyiswa isazi sezibalo saseJalimane u-Lothar Collatz ngo-1937. Uyinkinga yezibalo elula kakhulu ekuchazweni kwayo kodwa engakaxazululwa kuze kube manje, ethi noma iyiphi inombolo ephelele ephozithivu, ngemva kokuphindaphindwa kwemithetho ethile, ekugcineni izobuyela ku-1.
Imithetho yokubala ithi kunoma iyiphi inombolo ephelele ephozithivu n:
Uma u-n uyinombolo elinganayo, yihlukanise ngo-2 (n ÷ 2).
Uma u-n eyinombolo engalingani, yiphindaphinde ngo-3 bese wengeza u-1 (3n + 1).
Ngemva kokuthola inombolo entsha, phinda lezi zinyathelo kuze kube umphumela uba ngu-1.
Isibonelo ngenombolo 6:
U-6 uyinombolo elinganayo, uma uhlukaniswa ngo-2 uthola u-3
U-3 uyinombolo engalingani, uma uphindaphindwa ngo-3 bese kwengezwa u-1 uthola u-10
U-10 uyinombolo elinganayo, uma uhlukaniswa ngo-2 uthola u-5
U-5 uyinombolo engalingani, uma uphindaphindwa ngo-3 bese kwengezwa u-1 uthola u-16
U-16 uhlukaniswa ngo-2 ngokulandelana, kutholakale u-8, 4, 2, 1
Indlela yokugcina ithi: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.
Uchwepheshe wokuqinisekisa ngokusemthethweni u-Ramana Kumar washicilela iphrojekthi ku-GitHub ngoJulayi 25, ekuqaleni ethi ngosizo lwe-AI wayephikise umbono ka-Collatz. Iphrojekthi ayizange inikeze inombolo ethile ephikisa lo mbono, kodwa yamane yafakazela ku-Lean (uhlelo olusiza ekuqinisekiseni izimfundiso) ukuthi “kukhona inombolo engakwazi ukufinyelela ku-1”.
I-Lean iwuhlelo olusiza ekuqinisekiseni izimfundiso, oluvumela abasebenzisi ukuba babhale amafomula ezibalo nemiqondo enengqondo njengamakhodi, bese ikhompuyutha iqinisekisa ukunemba kobufakazi. Ikhodi ye-Lean ebhalwe ngumsebenzisi iguqula iziphakamiso zezibalo nobufakazi bube izinhlelo ezingahlolwa, kanti i-kernel iqinisekisa ukuvumelana kwezinhlobo nengqondo.
Nokho, ngesikhathi ehlola okuqukethwe okuphikisa lesi simangalo, wathola ukuthi le ndlela ingenza i-Lean yamukele ngaphandle kwemibandela i-“False” (emele isiphakamiso esingelona iqiniso). Ngakho-ke ikhodi ehambisana nalolu daba okwamanje ayikwazi ukuphikisa umbono ka-Collatz.
Umcwaningi wokuqinisekisa ngokusemthethweni u-Kiran Gopinathan wehlisa inkinga yaba ikhodi encane yokuyiphinda, wayibika eqenjini labathuthukisi be-Lean ngoJulayi 28, 2026.
Ubungozi babusengxenyeni ye-kernel ephatha “izinhlobo ezihlanganisiwe eziphindaphindwayo”, okwakwenza ngezinye izikhathi ingazinaki “amapharamitha ohlobo ayizipoki” (okungukuthi, amapharamitha angaveli ngokuqondile ezingxenyeni zesakhiwo sedatha), ngaleyo ndlela amapharamitha okwakufanele abhekwe njengamaphutha adlule ekuqinisekisweni. Umthuthukisi we-Lean u-Leonardo de Moura wathi inkinga yayiwukuthi ukuqaliswa kwe-kernel kwakungakaqedi ukuhlolwa okwakudingeka.
Iqembu le-Lean lakha isicelo sokudonsa sokulungisa le nkinga cishe ngemva kwehora elingu-1 lithole umbiko, lase likhipha inguqulo ye-Lean 4.32.2 ngoJulayi 28, elungisa le nkinga.