Anthropic: Claude Fermanın Son Teoreminin kompüterlə yoxlanılan sübutunu 11 gündə yazdı
Anthropic Fermanın Son Teoreminin tam və kompüterlə yoxlanılan ilk sübutunu paylaşıb: Claude Lean dilində 11 gün ərzində əsasən muxtar işləyib və 13 milyon sətir kod yaradıb.
Nə baş verdi
Anthropic Fermanın Son Teoreminin ilk tam və kompüterlə yoxlanılan sübutunu paylaşıb. Şirkətin məlumatına görə, Claude sübutu formal yoxlama üçün yaradılmış Lean dilində yazmaq üçün 11 gün ərzində əsasən muxtar çalışıb və 13 milyon sətir kod, 29 500 ara teorem yaradıb.
İşə Kolumbiya Universitetindəki qrupu ilə AI ilə formallaşdırma alətləri hazırlayan Anthropic tədqiqatçısı Tianyi Pen rəhbərlik edib. Sübut GitHub-da açıq şəkildə yerləşdirilib.
Niyə vacibdir
Fermanın fikri — n > 2 üçün aⁿ + bⁿ = cⁿ bərabərliyini ödəyən müsbət a, b, c tam ədədləri yoxdur — təqribən 1637-ci ildə yazılıb və Endryu Vayls onu yalnız 1995-ci ildə sübut edib: yoxlanması aylar çəkən 129 səhifə. Rieman hipotezi üzərində AI-ın yeni riyaziyyat yaratdığı son işindən fərqli olaraq, burada yenilik yoxlamadadır: formallaşdırılmış sübutu maşın yoxlayır.
Mütəxəssislər nə deyir
London İmperial Kollecinin tədqiqatçısı Kevin Bazzard, teoremin formallaşdırılması üzrə çoxillik icma layihəsinə rəhbərlik edir və bunu "fövqəladə avtoformallaşdırma nailiyyəti" adlandırıb: teorem riyaziyyatın aksiomlarından başqa heç bir fərziyyə olmadan sübut edilib. Anthropic-in sözlərinə görə, nəticə riyazi biliklərin yoxlanmasının və ona etimadın daha asan olacağı gələcəyə işarə edir.