Axiom Math формализовала доказательство теоремы классификации конечных простых групп

✔️ ИИ за 24 дня формализовал самое длинное доказательство в истории математики, над которым около 100 учёных работали десятилетиями. Компания Axiom Math объявила о завершении компьютерной проверки теоремы классификации конечных простых групп (CFSG), известной как «Огромная теорема». Оригинальное доказательство занимает 15 000 страниц в более чем 500 научных статьях. О чём вообще теорема? Представьте куб. Его можно повернуть 24 способами так, чтобы он выглядел точно так же. Эти преобразования образуют математическую группу. Теорема классифицирует фундаментальные «строительные блоки», из которых состоят все конечные группы симметрий. Это своеобразная периодическая таблица симметрий, применяемая в алгебре, теории чисел и математической физике. Что сделал ИИ: За 24 дня десятки ИИ-агентов создали около 43,1 млн строк кода на Lean. Формализовали доказательство, которое математики собирали на протяжении десятилетий. Обнаружили 34 существенных расхождения с опубликованными математическими работами. Нашли контрпримеры к некоторым утверждениям и разработали альтернативные доказательства. Получили новый результат в теории групп, необходимый для выбранного пути доказательства. В отдельных случаях ИИ обнаружил ошибки в исходных рассуждениях и построил новые математические аргументы, чтобы их исправить. Работа велась совместно с математиками, включая специалистов, участвовавших в первоначальной классификации. Результат Axiom представляет как первое полное доказательство CFSG, проверяемое компьютером. Код и материалы открыты для независимого изучения. Это пример того, как ИИ-агенты могут не только ускорять математическую работу, но и проверять фундаментальные результаты, которые раньше было практически невозможно перепроверить целиком. https://axiommath.ai/research/the-enormous-theorem-formalized/ @ai_machinelearning_big_data