• ИИ Anthropic формализовал доказательство Великой теоремы Ферма за 11 дней.
• Компания использовала языковую модель Claude для перевода доказательства Эндрю Уайлса и Ричарда Тейлора.
• Доказательство было формализовано на языке Lean и содержит 13 миллионов строк кода.
• Формализация доказательства на Lean позволяет компьютеру проверить его пошагово.
• С 2024 года математики работают над проектом MathLib, целью которого является полная формализация доказательства Уайлса и Тейлора.
• Anthropic заявляет, что модель «Клод» справилась с задачей за 11 дней и сгенерировала полностью верифицируемое доказательство.
• Код, созданный «Клодом», не является общедоступным и не интегрирован в MathLib, но его использование может упростить рецензирование статей.

«По мере того как научных статей становится все больше, а сами они — все длиннее и сложнее, процесс рецензирования отнимает больше времени, но при этом его качество снижается, — отметил Фредерик Маннерс, математик из Калифорнийского университета. — Появление у математиков своего рода „волшебной палочки“, способной получить статью с arXiv и либо выдать сертификат, подтверждающий ее корректность, либо указать на ошибку, принесло бы огромную пользу».