Anthropic. Claude-ը 11 օրում գրել է Ֆերմայի մեծ թեորեմի համակարգչով ստուգված ապացույցը
Anthropic-ը հրապարակել է Ֆերմայի մեծ թեորեմի առաջին ամբողջական, համակարգչով ստուգված ապացույցը. Claude-ը Lean լեզվով 11 օր աշխատել է հիմնականում ինքնավար՝ ստեղծելով 13 միլիոն տող կոդ։
Ինչ տեղի ունեցավ
Anthropic-ը հրապարակել է Ֆերմայի մեծ թեորեմի առաջին ամբողջական, համակարգչով ստուգված ապացույցը։ Ընկերության տվյալներով՝ Claude-ը 11 օր շարունակ հիմնականում ինքնավար աշխատել է, որպեսզի ապացույցը գրի Lean լեզվով՝ ֆորմալ ստուգման համար ստեղծված ծրագրավորման լեզվով, և ստեղծել է 13 միլիոն տող կոդ ու 29 500 միջանկյալ թեորեմ։
Աշխատանքը ղեկավարել է Anthropic-ի հետազոտող Տյանյի Պենը, ում խումբը Կոլումբիայի համալսարանում գործիքներ է ստեղծում արհեստական բանականությամբ ֆորմալացման համար։ Ապացույցը բացահայտ հրապարակված է GitHub-ում։
Ինչու է դա կարևոր
Ֆերմայի պնդումը՝ որ n > 2-ի դեպքում aⁿ + bⁿ = cⁿ հավասարումը դրական ամբողջ a, b, c թվերով լուծում չունի, գրվել է մոտ 1637 թվականին, և Էնդրյու Ուայլզը այն ապացուցել է միայն 1995-ին՝ 129 էջ, որի ստուգումը ամիսներ տևեց։ Ի տարբերություն Ռիմանի հիպոթեզի շուրջ AI-ի վերջին աշխատանքի, որտեղ նոր մաթեմատիկա ստեղծվեց, այստեղ նորությունը ստուգումն է. ֆորմալացված ապացույցը մեքենան է ստուգում։
Ինչ են ասում մասնագետները
Լոնդոնի Իմպերիալ քոլեջի Քևին Բազարդը, ով ղեկավարում է թեորեմի ֆորմալացման բազմամյա համայնքային նախաձեռնությունը, դա անվանել է «արտասովոր ինքնաֆորմալացման ձեռքբերում». թեորեմն ապացուցված է առանց մաթեմատիկայի աքսիոմներից բացի ոչ մի ենթադրության։ Anthropic-ի խոսքով՝ արդյունքը ցույց է տալիս ապագա, որտեղ մաթեմատիկական գիտելիքը ավելի հեշտ կլինի ստուգել և վստահել։