ИИ-агенты Axiom Math формализовали доказательство самой длинной теоремы в истории математики ⚠️ Теорема классификации конечных простых групп, или «Огромная теорема» — одно из крупнейших достижений математики XX века. Она классифицирует конечные простые математические группы — базовые элементы, из которых можно составить любую конечную группу, подобно тому, как составные числа раскладываются на простые множители. За 24 дня десятки ИИ-агентов под руководством инженеров и математиков создали около 43,1 миллиона строк кода на языке Lean, который позволяет компьютеру проверять математические доказательства. При формализации доказательства агенты обнаружили 34 существенных расхождения с опубликованными математическими работами, включая утверждения, для которых удалось построить контрпримеры. Чтобы завершить проверку, исследователям пришлось исправить часть рассуждений и разработать новые математические аргументы, в том числе получить новый результат в теории групп #Математика | #IT | *4.4 🙄 Подпишитесь на N + 1