Для этого потребовалось около 43,1 миллиона строк кода
Компания Axiom Math сообщила о завершении компьютерной формализации теоремы классификации конечных простых групп, или «Огромной теоремы» — одного из крупнейших достижений математики XX века. Теорема классифицируетИсходное доказательство «Огромной теоремы» занимает около 15 тысяч страниц в более чем 500 научных статьях, написанных примерно сотней математиков. конечные простые математические группы — базовые элементы, из которых можно составить любую конечную группу, подобно тому, как сложные числа раскладываются на простые множители. Работа над ее доказательством длится уже более полувека. В 1963 году американские математики Уолтер Фейт (Walter Feit) и Джон Томпсон (John Griggs Thompson) доказалиИх статья объемом 255 страниц заняла целый выпуск Pacific Journal of Mathematics., что порядок любой неабелевой конечной простой группы четен. Завершить классификацию в 1983 году смог Дэниел Горенстайн (Daniel Gorenstein), а в 2004 году Майкл Ашбахер (Michael Aschbacher) и Стивен Смит (Stephen D. Smith) опубликовали изложение объемом в 1221 страницу, завершив тем самым то, что стало известно как доказательство первого поколения. Именно его формализацией и занималась Axiom Math.
За 24 дня десятки ИИ-агентов под руководством инженеров и математиков создали около 43,1 миллиона строк кода на языке Lean, который позволяет компьютеру проверять математические доказательства. При формализации доказательства агенты обнаружили 34 существенных расхождения с опубликованными математическими работами, включая утверждения, для которых удалось построить контрпримеры. Чтобы завершить проверку, исследователям пришлось исправить часть рассуждений и разработать новые математические аргументы, в том числе получить новый результат в теории групп. В работе участвовали специалисты по теории групп, знакомые с первоначальным доказательством. Авторы проекта представили результат как первое полное компьютерно-проверяемое доказательство теоремы классификации конечных простых групп. Ранее мы рассказывали о том, как Модели OpenAI и Anthropic одновременно опровергли гипотезу экспоненциального времени.