Axiom заявила, что AI-агенты формализовали крупнейшее математическое доказательство в Lean
Компания выложила формализацию классификации конечных простых групп на 43,1 млн строк и попросила математиков независимо проверить её.
Axiom опубликовала то, что называет первым полным доказательством классификации конечных простых групп, проверяемым компьютером. Этот фундаментальный результат часто считают крупнейшим доказательством в истории математики: исходная классификация занимает около 15 000 страниц в более чем 500 работах примерно 100 математиков.
По данным Axiom, инженеры и математики 24 дня управляли десятками AI-агентов и получили около 43,1 млн строк кода на Lean. Lean проверяет, следует ли каждый шаг из явно заданных определений и допущений, и превращает аргумент из огромной литературы в единый граф зависимостей.
Формализация выявила опечатки, пропущенные условия и 34 более существенных расхождения с опубликованными работами. Axiom утверждает, что вопрос вокруг теоремы о несбалансированной группе потребовал серьёзной переработки, а проект дал новый результат в теории групп.
Компьютерная проверка не заменяет научную экспертизу. Нужно убедиться, что формулировка в Lean соответствует принятой классификации, а формализация выдерживает независимый аудит. Axiom предложила специалистам повторно запустить проверку и изучить определения. Если результат подтвердится, это станет примером научной работы AI-агентов масштаба, который один исследователь не смог бы проверить вручную.
