POINCARÉ, NA'URA TA DUBA SHI LAYI BAYAN LAYI

Duba hujja yana ɗaya daga cikin ayyuka mafi wahala a lissafi, musamman idan hujja ta shafi fannoni da dama. Yayin da AI ke hanzarta samar da hujjoji, ingantaccen tabbatarwa ya ƙara muhimmanci. Mataimakan hujja (proof assistants) kamar Lean 4 suna ba da amsa ɗaya: ana rubuta ma’anoni, bayanai da hujjoji a matsayin code, kuma wani ƙaramin ginshiƙi amintacce na manhajar, wato “kernel” ɗinta, yana duba kowane mataki. Hujjar da ta tsallake kernel ta tabbatar da bayaninta; abin da ya rage wa mutane shi ne duba cewa bayanin yana faɗar abin da masana lissafi ke nufi da gaske.

Hujja mai taƙaitawa, ɗakin karatu da ya ɓace

Hasashen Poincaré, wanda Perelman ya tabbatar, yana cewa kowane manifold mai girma uku a rufe kuma mai haɗuwa kai tsaye (simply connected) — a sauƙaƙe, wani sarari mai girma uku mai iyaka ba tare da ramukan da igiya mai da’ira za ta iya maƙalewa a ciki ba — daidai yake da ƙwallo mai girma uku. Hujjar tana bin shirin Ricci flow da Richard Hamilton ya fara. Takardun bincike uku na Perelman na 2002–2003 sun ba da muhimman hujjoji a taƙaice ƙwarai; bayanai dalla-dalla sun biyo baya, ciki har da littafin 2007 na John Morgan da Gang Tian da wannan aikin ke bi.

Wannan hujjar ta dogara ne da nazarin lissafin siffofi (geometric analysis) wanda ɗakin karatun al’ummar Lean, Mathlib, galibi bai da shi. Dole aka gina mafi yawan tushe daga farko.

Matakai masu muhimmanci da masana lissafi suka daskarar

Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu da abokan aikinsu a Jami’ar Peking da wasu cibiyoyin Beijing sun fara a watan Mayun 2026: “injiniyoyin AI” uku masu horon lissafi suna aiki tare da masana lissafi. Hanyarsu ta farko — mayar da manyan sassan ka’idojin tushe zuwa harshen kwamfuta — ta yi jinkiri, kuma code ɗin da ya fito bai kai abin da suke tsammani ba.

A watan Satumban 2026, sun sake farawa. An yanka hujjar zuwa kusan matakai masu muhimmanci 90 (milestones), kowanne bayani ne na Lean daidai tare da ma’anonin da yake buƙata. Masana lissafi sun duba waɗannan bayanai kafin ko yayin da ake mayar da su zuwa Lean, sannan aka daskarar da su: wakilan AI ba za su iya canza su ba, kuma duk wani gyara ya koma ta hannun masana lissafi. Tunda babu wanda zai iya karanta kowane layi da wakilan suka rubuta, waɗannan matakai sun zama wuraren duba inda mutane suka tabbatar da lissafin.

Daga nan wakilan suka yi aiki a lokaci ɗaya, ta zaman hulɗa da kayan aikin code — galibi Codex da Claude Code — da kuma ta wani tsari mai suna Archon Horizon da ke tura “ayyuka” masu iyaka zuwa sabobin (servers) da yawa. Wani bot ya haɗa kowace gudummawa kuma ya haɗa waɗanda aka karɓa. GPT-6-Astra ne ya ɗauki mafi yawan aikin mayar da bayanai zuwa Lean da gina hujjoji; an yi amfani da Fable-5.1 don dubawa mai zaman kansa, gano dalilin ayyukan da suka tsaya, da duba bayanai.

Layuka miliyan 2.8 cikin kusan makonni biyu

Bayan watannin shiri, babban aikin mayar da hujjar zuwa Lean ya ɗauki fiye da makonni biyu kaɗan. Kuɗin biyan AI da hayar sabobi ya kai kusan dala 25,000. Aikin ya tabbatar da duka nau’in topology da nau’in santsi (smooth) na theorem ɗin, yana haɗuwa gaba ɗaya kuma ya tsallake dubawa mai zaman kansa kan bayanan da aka nufa waɗanda aka rubuta da Mathlib kaɗai.

Yana da girma ƙwarai: kusan layuka miliyan 3.2 na Lean, an rage su zuwa miliyan 2.8 ta hanyar barin abin da theorem na ƙarshe ya dogara da shi kaɗai. A lissafin marubutan, kusan rabi ka’idojin tushe ne. Wani sakamako na gargajiya da Morgan da Tian suka ambata a cikin bayanin ƙasan shafi (footnote) guda ɗaya — game da tsarin santsi a kan manifolds masu girma uku — ya ɗauki kusan layuka 650,000 shi kaɗai.

Abin da mutane har yanzu suka yi

Marubutan sun raba matsalolin zuwa nau’i uku: giɓin lissafi, matsalolin aiwatarwa a Lean da matsalolin haɗin kai. Mutane ne suka ƙayyade iyakar bayanai (misali, lokacin da za a taƙaita sakamako zuwa girma uku), suka gano hujjojin da suka ɓace — kamar wani mataki na ƙanƙancewar wuri (local compactness) da wakilan ba su iya ganowa ba — kuma suka kama zato da aka ɓoye. Babban darasinsu: tsara aikin ya yi muhimmanci kamar ƙwarewar wakilan. Sun cimma irin wannan sakamako daga aikin Anthropic na baya-bayan nan na mayar da Theorem na Ƙarshe na Fermat zuwa harshen kwamfuta, wanda shi ma dole aka sake farawa bayan ƙoƙarin farko ya rasa bin halin da aikin ke ciki.

An tabbatar, amma ba a tsabtace ba tukuna

Marubutan ba sa ganin aikin ya ƙare. Code ɗin cike yake da maimaitawa; hujjojin wakilan ba koyaushe suke bin hanyar littafin da aka bi ba; kuma mayar da shi ɗakin karatu na nazarin lissafin siffofi da za a sake amfani da shi shi ne aiki na gaba. An kuma sanar da wani aikin mayar da wannan hasashe zuwa harshen kwamfuta mai zaman kansa daga wata tawaga. Fatansu: cewa wata rana masanin lissafi ɗaya zai iya amfani da irin waɗannan kayan aiki don tabbatar da bincikensa.

Rikicin moriya. Tawagar ta yi amfani da Claude Code da samfurin Fable-5.1, dukkansu daga Anthropic, tare da GPT-6-Astra, da aka yi amfani da shi ta biyan kuɗin OpenAI, wanda ya yi mafi yawan aikin. Takardar ta kuma kwatanta aikinta da aikin Anthropic na mayar da Theorem na Ƙarshe na Fermat zuwa harshen kwamfuta. Claude ne ya rubuta wannan labarin.