Claude формализовал доказательство Великой теоремы Ферма

Около 1637 года Пьер Ферма записал на полях книги утверждение, что натуральные числа a, b, c не могут удовлетворять уравнению aⁿ + bⁿ = cⁿ ни при каком n > 2. Ферма утверждал, что нашел доказательство, но полях было слишком мало места, чтобы его записать.

После этого математики искали это доказательство 350 лет. Впервые оно было найдено в 1995 году математиком Эндрю Уайлсом. Оно заняло 129 страниц. На самом деле он обнаружил его еще в 1993, но в процессе верификации был обнаружен пробел, над которым пришлось работать еще пару лет.

Проверка подобных сложных доказательств людьми может занимать годы. Есть способ проверять алгоритмически, но для этого доказательство нужно формализовать, то есть перевести на язык программирования (чаще всего на Lean). Однако это тоже очень сложно: нужно прописывать все шаги, даже тривиальные, и формализовать также все вложенные леммы. Математики редко делают это это в своих доказательствах, ссылаясь на "очевидность" и века нефомализованных утверждений.

Формализацию Великой теоремы Ферма уже пытались провести. Кевин Баззард начал этот процесс как многолетний проект сообщества. То есть ожидалось, что на формализацию уйдут годы и труд многих специалистов.

Вчера Anthropic объявили, что Claude полностью формализовал теорему за 11 дней. Автономно. Для этого он написал (внимание) 13 миллионов строк кода в Lean. Для сравнения: это в 5 раз больше, чем вся библиотека Mathlib. В процессе агенты также доказали 29 500 промежуточных лемм.

Тот самый Кевин Баззард, ознакомившись с доказательством, назвал это экстраординарным достижением автоформализации, и подтвердил, что теорема доказана без каких-либо допущений, кроме аксиом математики.

Кстати, на все про все у агентов ушло 6 миллиардов выходных токенов 🗿