POINCARÉ, IMEKAGULIWA MSTARI KWA MSTARI NA MASHINE

Kukagua uthibitisho ni moja ya kazi zinazodai zaidi katika hisabati, hasa hoja inapovuka fani kadhaa. Kadiri AI inavyoharakisha utengenezaji wa uthibitisho, uhakiki unaoaminika unakuwa muhimu zaidi. Wasaidizi wa uthibitisho (proof assistants) kama Lean 4 wanatoa jibu moja: fasili, kauli na uthibitisho huandikwa kama msimbo, na kiini kidogo kinachoaminika cha programu, “kerneli” yake, hukagua kila hatua. Uthibitisho unaopita kerneli huthibitisha kauli yake; kinachobaki kwa binadamu ni kukagua kuwa kauli hiyo kweli inasema kile wanahisabati wanachomaanisha.

Uthibitisho uliofupishwa, maktaba inayokosekana

Dhana ya Poincaré, iliyothibitishwa na Perelman, inasema kwamba kila namna-anuwai (manifold) ya pande tatu iliyofungwa na iliyounganishwa kisahili (simply connected) — kwa lugha rahisi, nafasi ya 3D yenye kikomo isiyo na tundu ambalo kitanzi kingeweza kunasa — ni sawa na tufe la pande tatu. Uthibitisho unafuata mpango wa mtiririko wa Ricci (Ricci flow) ulioanzishwa na Richard Hamilton. Machapisho matatu ya awali ya Perelman ya 2002–2003 yalitoa hoja kuu kwa namna iliyofupishwa sana; maelezo ya kina yalifuata, ikiwemo monografu ya mwaka 2007 ya John Morgan na Gang Tian ambayo mradi huu unaifuata.

Uthibitisho huo unategemea uchambuzi wa kijiometri ambao maktaba ya jumuiya ya Lean, Mathlib, kwa kiasi kikubwa haikuwa nao. Sehemu kubwa ya misingi ililazimika kujengwa kuanzia mwanzo.

Hatua muhimu zilizogandishwa na wanahisabati

Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu na wenzao katika Chuo Kikuu cha Peking na taasisi nyingine za Beijing walianza Mei 2026: “wahandisi wa AI” watatu wenye mafunzo ya hisabati wakifanya kazi pamoja na wanahisabati. Mbinu yao ya kwanza — kurasimisha vipande vikubwa vya nadharia ya msingi — ilikuwa ya polepole, na msimbo uliotokana nayo haukufikia matarajio yao.

Mwezi Septemba 2026, walianza upya. Uthibitisho ulikatwa katika takriban hatua muhimu 90, kila moja ikiwa kauli sahihi ya Lean pamoja na fasili inazohitaji. Wanahisabati walipitia kauli hizi kabla au wakati zilipokuwa zikirasimishwa, kisha zikagandishwa: mawakala hawakuweza kuzibadilisha, na marekebisho yoyote yalirudi kupitia kwa wanahisabati. Kwa kuwa hakuna aliyeweza kusoma kila mstari ulioandikwa na mawakala, hatua hizi muhimu zikawa vituo vya ukaguzi ambapo binadamu walihakiki hisabati.

Kisha mawakala walifanya kazi sambamba, kupitia vikao vya mwingiliano na zana za kuandika msimbo — hasa Codex na Claude Code — na kupitia mfumo uitwao Archon Horizon unaosambaza “misheni” zenye mipaka kwa seva nyingi. Boti ilikusanya (compile) kila mchango na kuunganisha ile iliyokubaliwa. GPT-6-Astra ilibeba sehemu kubwa ya urasimishaji wa kauli na ujenzi wa uthibitisho; Fable-5.1 ilitumika kwa ukaguzi huru, kutambua kazi zilizokwama na kupitia kauli.

Mistari milioni 2.8 katika takriban wiki mbili

Baada ya miezi ya maandalizi, urasimishaji mkuu ulichukua zaidi kidogo ya wiki mbili. Usajili wa AI na seva za kukodi viligharimu takriban dola 25,000. Kazi hii inathibitisha matoleo yote mawili ya nadharia, la kitopolojia na laini (smooth), inakusanyika kikamilifu na inapita ukaguzi huru dhidi ya kauli lengwa zilizoandikwa kwa kutumia Mathlib pekee.

Ni kubwa mno: takriban mistari milioni 3.2 ya Lean, iliyopunguzwa hadi milioni 2.8 kwa kubakiza tu kile ambacho nadharia ya mwisho inakitegemea. Kwa hesabu ya waandishi, karibu nusu ni nadharia ya msingi. Tokeo moja la kale ambalo Morgan na Tian wanalitaja katika tanbihi moja tu — kuhusu miundo laini kwenye namna-anuwai za pande tatu — lilichukua takriban mistari 650,000 peke yake.

Kile ambacho binadamu bado walifanya

Waandishi wanapanga vikwazo katika aina tatu: mapengo ya kihisabati, matatizo ya utekelezaji katika Lean na matatizo ya uratibu. Binadamu waliweka wigo wa kauli (kwa mfano, lini kuzuia tokeo kwa pande tatu tu), waligundua hoja zilizokosekana — kama hatua ya ushikamano wa eneo (local compactness) ambayo mawakala hawakuweza kuipata — na walinasa dhana zilizofichika. Somo lao kuu: mpangilio wa kazi ulikuwa muhimu kama uwezo wa mawakala. Wanafikia hitimisho hilo hilo kutokana na urasimishaji wa hivi karibuni wa Anthropic wa Nadharia ya Mwisho ya Fermat, ambao pia ulilazimika kuanza upya baada ya majaribio ya awali kupoteza ufuatiliaji wa hali ya mradi.

Imehakikiwa, lakini bado si nadhifu

Waandishi hawaioni kazi hii kuwa imekamilika. Msimbo umejaa marudio; uthibitisho wa mawakala haufuati kila mara njia ya marejeo; na kuugeuza kuwa maktaba ya uchambuzi wa kijiometri inayoweza kutumika tena ndiyo kazi inayofuata. Urasimishaji huru wa dhana hiyo hiyo na timu nyingine pia umetangazwa. Tumaini lao: kwamba siku moja mwanahisabati mmoja ataweza kutumia zana kama hizo kuhakiki utafiti wake mwenyewe.

Mgongano wa maslahi. Timu ilitumia Claude Code na modeli Fable-5.1, zote kutoka Anthropic, pamoja na GPT-6-Astra, iliyotumika kupitia usajili wa OpenAI, ambayo ilifanya sehemu kubwa ya kazi. Makala pia inalinganisha mradi wake na urasimishaji wa Anthropic wa Nadharia ya Mwisho ya Fermat. Makala hii imeandikwa na Claude.