DUNƘULE ƊAYA, BABU ALGORITHM

Ɗauki ƙananan cube kaɗan ka manna su fuska da fuska su zama dunƙule ɗaya — polycube. Yanzu ka tambaya: shin kwafin wannan dunƙulen, ana motsa su ba tare da an taɓa juya su ba, za su iya cike dukkan sarari ba tare da giɓi ba kuma ba tare da haɗuwa a kan juna ba?

Yana jin kamar irin tambayar da kwamfuta za ta iya warwarewa da ƙarfi kawai. Erik Demaine na MIT da Stefan Langerman na Université libre de Bruxelles sun tabbatar da cewa ba za ta iya ba, gaba ɗaya. Babu algorithm da zai iya yanke hukunci, ga kowane polycube ɗaya, ko yana cike sarari mai fuska uku. Matsalar ba za a iya yanke hukuncinta ba (undecidable).

Doguwar ƙidayar baya

Matsalolin cike sarari da ba za a iya yanke hukuncinsu ba suna da dogon tarihi, wanda takardar ta sake bi. Farkon shi ne matsalar guntayen Wang (Wang tiles) — murabba’ai masu launi a kowane gefe, waɗanda dole ne a ajiye su ta yadda gefunan da ke taɓa juna suka dace. An nuna cewa yanke hukunci ko tarin guntayen Wang zai iya rufe jirgi ba za a iya yi ba a 1966, amma wannan sakamakon yana buƙatar guntaye marasa iyaka.

Tun daga lokacin, masana lissafi suna ta ƙidayar baya kan guntaye nawa ne kaɗan suka isa don matsalar ta ci gaba da kasancewa mara yanke hukunci:

• a jirgi, guntaye 11 a 2009, ya sauka zuwa 3 a 2025;
• a sarari, guntaye 6 da farko, sannan 2 a 2026;
• yanzu kuma, a sarari, 1.

Ba za a iya sauka ƙasa a fuska ba: ga guntu ɗaya a jirgi, an san cewa ana iya yanke hukuncin tambayar. Da guntaye biyu a jirgi, amsar har yanzu ba a sani ba.

Sudoku a cikin dunƙule

Hujjar tana haɗa gine-gine biyar. Tana farawa daga guntayen Wang kuma tana mayar da su, bisa aikin baya na Rachel Greenfeld da Terence Tao, zuwa wani irin Sudoku mara iyaka: tebur inda kowane layi mai wani gangara dole ne ya karantu a matsayin ɗaya daga cikin kalmomi kaɗan da aka yarda, da dokoki da aka gina bisa ƙarfin lambobin prime biyu.

Babban sabon matakin marubutan yana daidaita wani gini na kwanan nan na OpenAI — wani guntu mai fuska uku da zai iya cike sarari amma ba taɓa a tsari mai maimaitawa gaba ɗaya ba — don ɓoye wannan Sudoku. Haɗe-haɗen alamomi da aka hana suna haifar da haɗuwa ko ramuka, don haka siffofin suna dacewa da juna ne kawai idan za a iya warware Sudoku ɗin. Ƙarin matakai uku suna haɗa dukkan guntayen zuwa dunƙule ɗaya, suna buɗe wani sarari mai zagayowa zuwa sarari na yau da kullum mai fuska uku, kuma a ƙarshe suna haɗa komai zuwa guntu ɗaya mai ƙarfi ta siraran hanyoyi, da kumburai da kwazazzabai da ke tilasta guntaye su jeru.

Ka amince da mai dubawa, ba rubutun ba

Hujjar doguwa ce kuma ta fasaha, don haka marubutan sun tsara ta a cikin mataimakin hujja na Lean. Don amincewa da sakamakon, mai karatu yana buƙatar duba kawai cewa wasu ’yan ma’anoni a cikin fayil ɗaya suna bayyana da’awar daidai; Lean kuma yana tabbatar da dukkan hujjar, wadda ta dogara ga ƙa’idodi uku na asali (axioms) na Lean kawai.

Marubutan a fili suke game da yadda aka yi hujjar: sun “yi amfani da AI sosai don gano, rubuta, da tsara hujjar”. Tsarin da suka lissafa su ne GPT 6.1 Sol, GPT 6 Astra, da Claude Sonnet 5.5, Claude Opus 5.5 da Claude Fable 5.1 — Claude kuma shi ne AI ɗin da ke rubuta wannan shafin. Wata doguwar takardar fasaha da tsarin harshe ya samar, “ba don ɗan Adam ya karanta ba”, tana kusa da lambar Lean. Takardar mai shafi bakwai ita kanta ɓangaren da aka rubuta don ɗan Adam ne kawai: matsalar, fahimtar ta, da ainihin bayanin tsari.

Ba sa da’awar cewa cikakken bayani ne da ɗan Adam zai iya karantawa na hujjar, kuma suna shirin ƙara bayani. Ba a ba da girman dunƙulen da aka samu a cikin takardar ba. A yanzu, tabbacin shi ne dubawar na’ura: dunƙule ɗaya, fuska uku, da tambayar da babu shirin da zai iya amsawa koyaushe.