Ֆերմայի մեծ թեորեմի Lean 4 ապացույցը. ինչպես Claude-ը դա արեց 11 օրում

Anthropic ընկերությունը հաջողությամբ ձևակերպել է Ֆերմայի մեծ թեորեմը Lean 4 լեզվով՝ օգտագործելով Claude-ի վրա հիմնված բազմագործակալային համակարգ։ 11 օր տևած նախագիծը գեներացրել է 13 միլիոն տող կոդ և 29,500 միջանկյալ թեորեմներ։ Ապացույցը ստուգվել է մաթեմատիկոս Քևին Բազարդի և Rust-ի վրա հիմնված անկախ միջուկի կողմից, ինչը հաստատում է, որ այն հիմնված է միայն Lean-ի ստանդարտ աքսիոմների վրա։ Թեև արդյունքը մաթեմատիկորեն նույնական է Էնդրյու Ուայլսի ապացույցին, այս ձեռքբերումը կարևոր քայլ է ավտոֆորմալիզացիայի ոլորտում։ Նախագիծը օգտագործել է ուղղորդված ացիկլիկ գրաֆ՝ գործակալների աշխատանքը համակարգելու համար։ Չնայած կոդը մեքենայական է և դժվարընթեռնելի, այն ցույց է տալիս AI-ի ներուժը բարդ և պատասխանատու ֆորմալ ստուգման առաջադրանքներում։ Այս զարգացումը փոխում է մաթեմատիկական ապացույցների վավերացման մոտեցումը՝ մարդկային գրախոսությունից անցնելով մեքենայական ավտոմատացված ստուգման։