С 13 миллионами строк кода за 11 дней: Клод формулирует великую теорему Ферма

Анонсировано, что модель искусственного интеллекта "Клод" от компании "Антропик" смогла за 11 дней практически независимо сформулировать величайшую теорему Ферма в виде программного кода.

В результате было создано около 13 миллионов строк программного кода на языке "Лин", а также примерно 29 500 промежуточных теорем, что эквивалентно примерно пятикратному объёму всей официальной математической библиотеки "Mathlib".

Напомним, что французский математик Пьер де Ферма сформулировал эту теорему в XVII веке, однако её доказательство оставалось недостижимым более чем три столетия, пока британский математик Эндрю Уайлз не смог его найти в 1995 году после почти семи лет работы над ней в тайне.

Формальное представление означает перевод математического доказательства в компьютерный код, позволяющий компьютеру проверить правильность каждого шага.

Многие математики пытались найти доказательство этой задачи, но все их попытки заканчивались неудачей. Уайлз работал над проблемой втайне в течение семи лет, прежде чем объявить о крупном прорыве в 1993 году. Как правило, математические доказательства состоят из длинных цепочек логических рассуждений, где каждое последующее утверждение зависит от предыдущего, так что ошибка в одной из частей может привести к полному разрушению всего доказательства.

Как раз это и произошло с Уайлзом, когда была обнаружена уязвимость в его доказательстве, и потребовался почти год, чтобы её устранить.

Цифровизация математических теорий, или формализация, переводит их из мира бумаги и ручки в мир программного кода, позволяя компьютерам обрабатывать их и проверять логическую корректность пошагово, выявляя любые ошибки или уязвимости. Центральный репозиторий "Mathlib" содержит около двух миллионов строк формально оформленной математики.

Профессор Кевин Базард из Имперского колледжа Лондона потратил пять лет на выполнение этой задачи, тогда как модель "Клод" справилась с ней за 11 дней. По словам Базарда, доказательство "не опирается ни на что, кроме аксиом математики".

Задача была разделена между агентами искусственного интеллекта, которые получали общие указания периодически, а помощь в координации работы оказывала система "Prove2Me", изначально разработанная для поддержки человеческих математиков.

Если эти результаты окажутся воспроизводимыми надёжно, искусственный интеллект сможет ускорить процесс перевода современной математики в формы, пригодные для автоматической проверки.