AI şirkəti Anthropic Fermatın son teoremasının formalaşdırılmış sübutunu yaratdı. Bir qrup süni intellekt agentinin bu işi başa çatdırması yalnız 11 gün çəkdi. Bu da 1990-cı illərdə təklif olunan insan tərəfindən tapılan sübutun doğruluğunu təsdiqlədi.
Fermatın son teoreması, 1995-ci ildə Andrew Wiles tərəfindən sübut edilənə qədər əsrlər boyu riyaziyyatçıları qarışdırırdı. O, a, b və c ədədlərinin bir + bn = cn tənliyini təmin edən tam sayın olmadığını, burada n 2-dən böyük bir tam saydır.
Teoremi demək asan olsa da, sübut etmək çox çətin idi. Riyazi Pierre de Fermat 17-ci əsrdə bu puzlunu ortaya qoydu və onun yazdığı dərsliyin kənarlarına uyğunlaşmaq üçün çox böyük olduğunu söyləyərək, tapdığını iddia etdiyi bir sübutuna istinad etdi.
Riyaziyyat tarixində ən böyük dəyişikliklərə məruz qalır.
Bir çox riyaziyyatçı bir sübut tapmağa çalışdı və buna nail olmadı. Wiles 1993-cü ildə öz qələbəsini elan etməzdən əvvəl problemlə 7 il gizli işləyib. Əldə edilən sübutlar tez-tez bir-birinə əsaslanan uzun məntiqi mübahisələrə səbəb olur. Əgər bir addımda səhv varsa, bütün şey çökə bilər. Bu Wiles-ə də baş verdi, sübutlarında bir çatışmazlıq tapıldıqda onu və əməkdaşı Richard Tayloru düzəltmək üçün təxminən bir il vaxt lazım oldu.
Riyaziyyat nəzəriyyələrinin formalaşdırılması bu problemin həllidir. Onları qələm və kağız sahəsindən çıxarır və maşınların onlarla mübarizə aparmasına imkan verən bir konfigüraciyaya qoyar. Mathlib adlı mərkəzi bir depoda saxlanan 2 milyon xətti formalizasiya edilmiş riyaziyyata malikdir.
Xülasə — davamını mənbədə oxuyun.
