🤖 ИИ за 24 дня формализовал самое длинное доказательство в истории математики
Axiom Math объявила о первом компьютерно-проверяемом доказательстве классификации конечных простых групп (CFSG, «Огромная теорема») в Lean. Рой агентов AxiomProver за 24 дня сгенерировал около 43,1 млн строк кода: 108 вех, ~380 задач, под руководством математиков. В классическом доказательстве (~15 000 страниц) нашлись 34 существенных расхождения с литературой, а 10 октября агенты доказали простоту группы Монстра.
🌍 Формализация выявила реальные пробелы в опубликованных работах, а связка роя агентов с Lean превращает многолетнюю проверку теорем в управляемый процесс.
👤 ИИ уже пишет доказательства и находит контрпримеры, но это пока заявление одной компании без независимого рецензирования.
Источник 1: https://axiommath.ai/research/the-enormous-theorem-formalized/ Источник 2: https://cryptobriefing.com/axiom-ai-formalizes-enormous-theorem-24-days/