Математик Кевин Баззард получил грант в размере около одного миллиона фунтов стерлингов на формализацию и верификацию теоремы Ферма (2024-2029гг)/ Его сообщение после того, как Антропик заявила о завершении формализации и верификации теоремы в Lean 4.
https://xenaproject.wordpress.com/2026/ ... -me-to-it/Текст перевел ИИ.
Цитата:
ВТФ: Anthropic меня опередила
Опубликовано 4 сентября 2026 года автором xenaproject
Полагаю, технически первым миру об этом сообщил один кофейный магазин в Ислингтоне через Instagram, но час спустя Anthropic сделала официальное объявление: одна из их внутренних моделей, используя платформу prove2.me, формализовала в Lean полное доказательство Великой теоремы Ферма (ВТФ, FLT).
Это последняя теорема из знаменитого списка 100 задач по формализации Фрека Вейдейка (Freek Wiedijk), которая оставалась неформализованной; таким образом, этот двадцатилетний бенчмарк теперь полностью завершён. Поздравляю Anthropic!
Математические детали
Доказательство — не современное, которое я сам формализую, следуя идеям Khare, Taylor и других, а изложение Darmon–Diamond–Taylor 1995 года аргумента Wiles–Taylor–Wiles, использующего теорему Langlands–Tunnell и теорему Рибе о понижении уровня.
В репозитории Anthropic развивается теория Фонтена — для изучения плоских деформаций представлений Галуа — и формализуется достаточная часть работ Мазура об эйзенштейновом идеале, чтобы доказать, что никакая кривая Фрея не может иметь точку порядка p ≥ 17.
Это означает, что их доказательство ВТФ работает только для p ≥ 17. Однако ВТФ уже была формализована для нечётных регулярных простых в работе Best–Birkbeck–Brasca–Rodriguez–van-der-Velde–Yang, а наименьшее нерегулярное простое равно 37, так что всё в порядке.
Кодовая база
Я скомпилировал кодовую базу и запустил на ней comparator — проверка проходит успешно.
Это гигантское доказательство — более 13,4 миллиона строк кода, — и его компиляция занимает почти в 20 раз больше времени, чем компиляция математической библиотеки Lean (на машине с 96 ядрами!).
Lean может работать довольно медленно при переходах от файла к файлу в репозитории такого размера — даже на машине с 500 ГБ оперативной памяти, доступ к которой Anthropic мне также предоставила. Однако Anthropic также передала мне несколько HTML-документов, по которым на практике ориентироваться проще: клонируйте репозиторий и откройте их в веб-браузере.
Что представляет собой эта работа — и чем она не является
В настоящее время EPSRC финансирует мою работу по формализации доказательства Великой теоремы Ферма, и наивной реакцией на приведённую выше новость могло бы быть предположение, что теперь мне больше нечего делать. Это не так.
Эта работа, безусловно, достигает некоторых целей проекта EPSRC и действительно идёт значительно дальше по объёму формализованного материала. Я обещал EPSRC лишь свести ВТФ к результатам 1980-х годов; этот же репозиторий доказывает её полностью.
Но я также обещал EPSRC несколько других вещей. Во-первых, я должен отправлять pull request'ы в математическую библиотеку Lean, добавляя фундаментальные объекты современной теории чисел; эта работа продолжается.
Во-вторых — и, возможно, это самое важное, — я должен создать динамический документ, позволяющий людям исследовать современное доказательство. Полагаю, маловероятно, что Anthropic станет этим заниматься: скорее всего, они сочтут свою работу завершённой после формализации (к тому же современное доказательство они всё равно не формализовали).
Заметьте, что с математической точки зрения эта работа Anthropic практически ничего нового нам не сообщает. Я публично говорил, что на 99,9% уверен в корректности доказательства ВТФ, а большинство специалистов по теории чисел уверены в нём на 100% (формализация сделала меня более подозрительным по отношению к математической литературе, чем большинство моих коллег).
Насколько я понимаю этот аргумент, формализация просто добросовестно следует ранней литературе, посвящённой доказательству, и ничего к ней не добавляет.
Но эта работа действительно показывает нам, что теперь возможно в области автоматической формализации.
Если уже сегодня некая система из множества ИИ способна за 11 дней от начала до конца формализовать тысячи страниц математической литературы, то в будущем мы начнём видеть формализацию современных исследований практически по мере их появления.
Мы также узнаем, оправдана ли моя паранойя относительно нынешнего состояния программы Ленглендса, когда машины начнут проверять её и безжалостно отмечать неполные аргументы.
Возможность автоматически формализовать сложный материал в конечном счёте сделает процесс рецензирования математических статей гораздо менее мучительным.
Кроме того, это заставит нас быть предельно честными и аккуратными: существуют статьи, которые опираются на результаты, якобы «известные специалистам», и будет интересно увидеть, что именно на самом деле предполагается в доказательствах различных важных результатов в моей области.
Вот почему эта новость так меня радует!
Мне выделили £1 млн на выполнение моего проекта в течение пяти лет; Anthropic понадобилось всего 11 дней, хотя мне всё-таки интересно, не потратили ли они больше денег…
Небольшая история
Мне показалось, что будет неплохо закончить личной историей.
В 1993 году Уайлс объявил о своём доказательстве ВТФ в Институте Ньютона в ходе серии из трёх лекций. Я присутствовал на первой — тогда я был аспирантом второго года обучения — и не понял практически ничего, поэтому две следующие лекции пропустил и вместо этого уехал отдыхать в Ирландию со своей новой девушкой.
Я был настолько влюблён, что совершенно забыл обо всех слухах, и только вернувшись через неделю в Кембридж, узнал новость о том, что теорема доказана.
Что-то странно похожее произошло и на этот раз.
Когда мне пришло письмо от Anthropic, я находился в Уэльсе на музыкальном фестивале Green Man с той же самой девушкой, но мобильная связь там была очень плохой.
В короткий момент, когда появился 4G, я всё-таки заметил письмо от человека, о котором никогда прежде не слышал, с темой «End-to-end Lean formalization of Fermat's Last Theorem» («Полная сквозная формализация Великой теоремы Ферма в Lean»), но решил, что его написал какой-то чудак!
Лишь неделю спустя, разбирая почти тысячу непрочитанных писем, накопившихся за время моего отсутствия, я узнал эту новость.
) сформулировал эпсилон-гипотезу (ЭГ) и показал, что из ЭГ и ГТС следует ВТФ.