С помощта на един от своите AI модели (Claude), Anthropic създаде версия на изключително сложно математическо доказателство, която може да бъде проверена на компютър.

Доказателството, върху което Anthropic работи в рамките на този проект потвърждава хипотезата, известна като Последната теорема на Ферма – тя е формулирана през 1637 година и е свързана със свойствата на положителните цели числа. Доказателството на теоремата е разработено през 1995 година от математика Андрю Уайлс – то се състои от 129 страници, а проверката му отнема няколко месеца работа. В рамките на изследователския проект на Anthropic успяха да формализират доказателството на Уайлс, т.е. да го преобразуват във форма, която може да бъде проверена на компютър.

Формализираното доказателство представлява код, написан на езика за програмиране Lean – размерът му е 13 милиона реда, което е най-големият обем в цялата история. Формализацията е сложна, защото доказателствата по правило са доста лаконични – в нея липсват някои обяснения, необходими на компютъра за разбиране, което налага те да се добавят ръчно. Аргументите в доказателството често произтичат един от друг, т.е. грешка в един ред на Lean може да направи невалиден целия последващ код.

Математиците предполагаха, че формализирането на доказателството на Уайлс ще отнеме няколко години, но изследователският модел на Anthropic изпълни задачата за 11 дни – по-точно, това беше AI модел, сравним с общодостъпния Claude Fable 5.1.

AI моделът изпълни задачата, използвайки само ограничен обем данни на високо ниво. Той стартира няколко десетки агенти, които генерираха 6 милиарда токена изходни данни и в процеса доказаха 29 500 междинни теореми. Първият опит завърши с неуспех, но пробивът беше постигнат, когато на Claude беше предоставен достъп до платформата Prove2Me.

„Видяхме автоформализация на алгебрата, хармоничния анализ, геометрията и теорията на числата и разбрахме, че средствата за автоформализация вече са достатъчно надеждни, за да може да се работи с тях – доказателството е многостепенно.“

заяви математикът Кевин Базард, чиято работа беше използвана в проекта.

Освен това, миналия месец Anthropic отбеляза напредък в доказването на хипотезата на Риман – повече по тази тема можете да прочетете тук.