В 1637 году математик Пьер де Ферма выдвинул утверждение о равенстве $x^n + y^n = z^n$, где $x$, $y$, $z$ и $n$ — положительные целые числа. Ферма утверждал, что для этого уравнения не существует допустимого решения, если показатель степени $n$ больше 2.
Это означает, что не существует комбинации значений для $x$, $y$ и $z$, которая сделала бы это утверждение истинным; по мнению Ферма, сумма $x^n$ и $y^n$ никогда не даст $z^n$. Необходимость того, чтобы $n$ было больше 2, можно противопоставить теореме Пифагора ($x^2 + y^2 = z^2$), которая верна, как показано примером $3^2 + 4^2 = 5^2$, доказывая, что опровержение Ферма не применимо, когда $n=2$.
Ферма постулировал, что невозможность решений сохраняется для $n=3$, $n=4$ и других больших значений, но он так и не записал доказательство, которое имел в виду. Эта концепция известна как Великая теорема Ферма. Потребовалось 357 лет, чтобы кто-либо доказал корректность Ферма, причем Эндрю Уайлс завершил доказательство в 1994 году — событие, считающееся научным прорывом XX века. За это достижение Уайлс получил Премию Абеля в 2016 году.
Недавно прототип модели искусственного интеллекта Claude преобразовал это доказательство в проверяемый код, состоящий из 13 миллионов строк. Компания Anthropic, разработчик Claude, опубликовала это объявление 4 сентября. ИИ потратил всего 11 дней на завершение проекта, в то время как по оценкам, людям потребовалось бы около 10 лет для выполнения той же работы.
Важно отметить, что Claude не решил проблему, а лишь формализовал ее доказательство. Он преобразовал доказательство, изначально написанное на естественном языке (словами), в формальное доказательство, поддающееся вычислительной проверке, по сути, переведя человеческий аргумент на логический язык машин с использованием языка программирования с открытым исходным кодом Lean.
Эта формализация вносит вклад в растущий корпус достижений ИИ в математике, помогая как человеческим исследователям, так и генерируя новые рассуждения. Кевин Баззард, математик Имперского колледжа Лондона, в интервью Nature прокомментировал, что два года назад такая способность все еще считалась фантастикой. Исследователь Баззард работает над формализацией теоремы Ферма в Lean с 2024 года.
Чтобы формализовать математическое доказательство в Lean, система должна знать предыдущие концепции, аргументы и доказательства, поскольку математические знания строятся на уже подтвержденных утверждениях. Чтобы справляться с все более сложными доказательствами, математики разработали Mathlib — библиотеку формализаций в Lean, включения которой проходят кураторство со стороны экспертов-людей.
Ранее проверка математических доказательств полностью зависела от экспертов-людей, которые тратили годы на проверку логической цепочки аргументов. Однако многие доказательства публикуются в менее известных журналах, что ограничивает их охват и оставляет их действительность неопределенной, что препятствует прогрессу в некоторых областях математики, зависящих от них. Многие математики надеются, что сочетание формализации с помощью ИИ, Mathlib и человеческой проверки может оптимизировать работу рецензентов научных журналов и ускорить математический прогресс.