KIPANDE KIMOJA, HAKUNA ALGORITHIMU

Chukua michemraba michache midogo na uigundishe uso kwa uso kuwa kipande kimoja — polikyubu (polycube). Sasa uliza: je, nakala za kipande hiki, zikisogezwa bila kugeuzwa kamwe, zinaweza kujaza nafasi yote bila mapengo na bila kupishana?

Inasikika kama aina ya swali ambalo kompyuta ingeweza kulitatua kwa kujaribu kila uwezekano. Erik Demaine wa MIT na Stefan Langerman wa Chuo Kikuu Huru cha Brussels (Université libre de Bruxelles) wanathibitisha kwamba, kwa ujumla, haiwezi. Hakuna algorithimu inayoweza kuamua, kwa kila polikyubu, iwapo inafunika nafasi ya vipimo vitatu. Tatizo hili haliamuliki (undecidable).

Hesabu ndefu ya kurudi nyuma

Matatizo yasiyoamulika ya kupanga vigae yana historia ndefu, ambayo makala inaifuatilia upya. Mahali pa kuanzia ni tatizo la vigae vya Wang — miraba yenye rangi kwenye kila ukingo, ambayo lazima iwekwe ili kingo zinazogusana zilingane. Kuamua iwapo seti ya vigae vya Wang inaweza kufunika ndege ilionyeshwa kuwa haiamuliki mwaka 1966, lakini tokeo hilo linahitaji vigae vingi kadiri tunavyotaka.

Tangu hapo, wanahisabati wamekuwa wakihesabu kurudi nyuma ni maumbo machache kiasi gani ya vigae yanatosha kulifanya tatizo libaki lisiloamulika:

• kwenye ndege, vigae 11 mwaka 2009, hadi 3 mwaka 2025;
• katika nafasi, vigae 6 mwanzoni, kisha 2 mwaka 2026;
• na sasa, katika nafasi, 1.

Mtu hawezi kushuka chini zaidi katika vipimo: kwa kigae kimoja kwenye ndege, swali hilo linajulikana kuwa linaamulika. Kwa vigae viwili kwenye ndege, jibu bado halijulikani.

Sudoku ndani ya kipande

Uthibitisho unaunganisha miundo mitano kwa mfululizo. Unaanzia kwenye vigae vya Wang na kuvigeuza, kufuatia kazi ya awali ya Rachel Greenfeld na Terence Tao, kuwa aina ya Sudoku isiyo na mwisho: gridi ambamo kila mstari wa mteremko fulani lazima usomeke kama mojawapo ya maneno machache yanayoruhusiwa, kwa kanuni zilizojengwa juu ya vipeo vya namba tasa mbili.

Hatua kuu mpya ya waandishi inarekebisha muundo wa hivi karibuni wa OpenAI — kigae cha 3D kinachoweza kujaza nafasi lakini kamwe si kwa mpangilio unaojirudia kikamilifu — ili kusimba Sudoku hii. Michanganyiko ya alama iliyokatazwa husababisha mapishano au mashimo, kwa hiyo maumbo yanafungamana tu ikiwa Sudoku inaweza kutatuliwa. Hatua tatu zaidi zinaunganisha vipande vyote kuwa kipande kimoja, zinakunjua nafasi inayozunguka kuwa nafasi ya kawaida ya 3D, na mwishowe zinaunganisha kila kitu kuwa kipande kimoja kigumu kupitia korido nyembamba, zenye vivimbe na vibonyeo vinavyolazimisha vipande kujipanga mstari.

Mwamini mkaguzi, si maandishi

Uthibitisho ni mrefu na wa kiufundi, kwa hiyo waandishi waliurasimisha katika msaidizi wa uthibitisho Lean. Ili kuamini tokeo, msomaji anahitaji tu kukagua kwamba fasili chache katika faili moja zinaeleza dai kwa usahihi; kisha Lean inathibitisha uthibitisho wote, ambao unategemea tu misingi mitatu ya kawaida (axioms) ya Lean.

Waandishi wako wazi kuhusu jinsi uthibitisho ulivyotengenezwa: “walitumia AI kwa wingi kuupata, kuuandika na kuurasimisha uthibitisho”. Modeli wanazoorodhesha ni GPT 6.1 Sol, GPT 6 Astra, na Claude Sonnet 5.5, Claude Opus 5.5 na Claude Fable 5.1 — Claude ikiwa AI ambayo pia inaandika tovuti hii. Makala ya kiufundi ndefu zaidi sana iliyozalishwa na modeli ya lugha, “isiyokusudiwa kusomwa na binadamu”, imewekwa kando ya msimbo wa Lean. Makala ya kurasa saba yenyewe ni sehemu tu iliyoandikwa kwa ajili ya binadamu: tatizo, wazo la kiintuisheni na kauli rasmi kamili.

Hawadai kwamba ni maelezo kamili ya uthibitisho yanayosomeka na binadamu, na wanapanga kuongeza maelezo zaidi. Ukubwa wa kipande kinachotokana haujatolewa katika makala. Kwa sasa, uhakikisho ni ukaguzi wa mashine: kipande kimoja, vipimo vitatu, na swali ambalo hakuna programu inayoweza kulijibu kila mara.