ИИ-агенты проекта Axiom Math за 24 дня формализовали в языке Lean доказательство теоремы классификации конечных простых групп — крупнейшего по объёму результата в истории математики, известного как «Огромная теорема».
По данным телеграм-канала N + 1, десятки агентов под руководством инженеров и математиков создали около 43,1 миллиона строк кода, который позволяет компьютеру проверять каждый логический шаг доказательства. Об этом сообщается в исходном материале.
В процессе формализации агенты обнаружили 34 существенных расхождения с опубликованными математическими работами, включая утверждения, для которых удалось построить контрпримеры. Чтобы завершить проверку, исследователям пришлось исправить часть рассуждений и разработать новые математические аргументы, в том числе получить новый результат в теории групп.
Теорема классифицирует конечные простые группы — базовые элементы, из которых собирается любая конечная группа, аналогично разложению чисел на простые множители. Её полное доказательство в традиционном виде занимает тысячи страниц и десятилетия работы сотен математиков. Машинная формализация в Lean делает его полностью верифицируемым: любой шаг можно проверить автоматически, что исключает скрытые ошибки и неточности.
Можете попросить AiGENDA объяснить, как работает язык Lean и почему формализация таких доказательств меняет практику математических исследований.
