Claude Inafanya Kanuni ya Mwisho ya Fermat kuwa Rasmi katika Lean

Anthropic hivi karibuni imekamilisha kazi kubwa ya utafiti. Modeli ya ndani ilifanya kazi kwa siku 11 ili kuifanya Kanuni ya Mwisho ya Fermat kuwa rasmi kwa kutumia lugha ya uthibitisho ya Lean 4.

Hii si ugunduzi mpya wa kihisabati. Andrew Wiles alithibitisha kanuni hii mnamo 1995. Kile ambacho Anthropic ilifanya ni kutafsiri uthibitisho huo uliopo kuwa kodi. Hii inaruhusu kompyuta kukagua kila hatua ya kimantiki kwa uhakika kamili.

Ukubwa wa mradi huu ni mkubwa sana: • Modeli hiyo ilizalisha mistari milioni 13 ya kodi ya Lean. • Ilithibitisha nadharia 30,300 za kati. • Ilitumia karibu tokeni bilioni 6 za matokeo.

Modeli hiyo ilifanya kazi kwa kiasi kikubwa yenyewe. Binadamu walitoa tu maelekezo ya kiwango cha juu mara chache. Mchakato huo uliisha katikati ya usiku wakati hakuna mtu aliyekuwa akitazama. Mfumo uliandikisha mafanikio hayo kiotomatiki.

Mambo mawili muhimu ya kuzingatia:

  1. Modeli hii ni chombo cha utafiti wa ndani. Huwezi kuipata kupitia API bado. Sio sawa na modeli za Claude unazotumia leo.
  2. Thamani halisi kwa watengenezaji iko katika tabaka la uratibu linaloitwa Prove2Me.

Prove2Me ni chombo cha chanzo huru. Kinatumia grafu ya utegemezi kusimamia kazi. Badala ya orodha rahisi ya ukaguzi, kinatengeneza ramani ya jinsi uthibitisho unavyounganishwa mmoja na mwingine.

Muundo huu unatatua matatizo mawili makuu kwa mifumo ya kazi ya mawakala (agent workflows):

  • Unazuia mawakala wengi kufanya kazi ile ile.
  • Unawapa mawakala kumbukumbu ya pamoja ili wasisahau lengo kuu.

Mifumo mingi ya kazi ya mawakala hushindwa kwa sababu hupoteza muktadha (context) baada ya muda. Kutumia grafu ya nje ya pamoja badala ya dirisha refu la mazungumzo (chat window) kunaweka kazi kwenye mstari sahihi.

Unapaswa kujifunza usanifu wa Prove2Me ikiwa unajenga mifumo ya kazi ya mawakala. Hata kama hutumii modeli za utafiti za Anthropic, jinsi wanavyoratibu kazi ni mwongozo kwa kazi za muda mrefu.

Chanzo: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36

Jumuiya ya kujifunza ya hiari: https://t.me/GyaanSetuAi