Anthropic-მა ფერმას დიდი თეორემის პირველი კომპიუტერით შემოწმებული დამტკიცება წარმოადგინა

რა მოხდა

Anthropic-მა გამოაქვეყნა ფერმას დიდი თეორემის პირველი სრული, კომპიუტერით შემოწმებული დამტკიცება. კომპანიის ცნობით, Claude-მა 11 დღის განმავლობაში თითქმის ავტონომიურად დაწერა დამტკიცება Lean-ის ენაზე — ფორმალური ვერიფიკაციისთვის შექმნილ პროგრამირების ენაზე — და შედეგად 13 მილიონი ხაზი კოდი და 29 500 შუალედური თეორემა მიიღო.

სამუშაოს ხელმძღვანელია Anthropic-ის მკვლევარი ტიანი პენი, რომლის ჯგუფი კოლუმბიის უნივერსიტეტში AI-ით ფორმალიზაციის ინსტრუმენტებს ქმნის. დამტკიცება ღიად არის გამოქვეყნებული GitHub-ზე.

რატომ არის მნიშვნელოვანი

ფერმას მტკიცება — რომ ვერ მოიძებნება დადებითი მთელი რიცხვები a, b, c, სადაც aⁿ + bⁿ = cⁿ n > 2-ისთვის — 1637 წლით თარიღდება; ენდრიუ უაილზმა ის მხოლოდ 1995 წელს დაამტკიცა — 129 გვერდი, რომლის გადამოწმებას თვეები დასჭირდა. რიმანის ჰიპოთეზაზე ბოლო AI მუშაობისგან განსხვავებით, სადაც ახალი მათემატიკა შეიქმნა, აქ სიახლე ვერიფიკაციაა: ფორმალიზებული დამტკიცება მანქანით მოწმდება.

რას ამბობენ ექსპერტები

კევინ ბაზარდი (იმპერიალ კოლეჯი ლონდონი), რომელიც თეორემის ფორმალიზაციის მრავალწლიან საზოგადოებრივ პროექტს ხელმძღვანელობს, ამას „არაჩვეულებრივ ავტოფორმალიზაციის მიღწევას" უწოდებს — თეორემა დამტკიცებულია მათემატიკის აქსიომების გარდა სხვა დაშვებების გარეშე. Anthropic-ის თქმით, შედეგი მიუთითებს მომავალზე, სადაც მათემატიკური ცოდნის შემოწმება უფრო ადვილი და სანდო გახდება.

📖 წყარო