Axiom заявляет, что ИИ-агенты формализовали классификацию конечных простых групп на Lean

Axiom, компания в сфере ИИ и математики, объявила в X о полной автоматической формализации классификации конечных простых групп на Lean — результата, который она называет «периодической таблицей симметрии». По словам компании, исходное доказательство занимало около 15 000 страниц, а над ним на протяжении нескольких поколений работали более 100 математиков. Axiom называет его крупнейшим математическим доказательством в истории, прошедшим компьютерную проверку.

Согласно репозиторию Axiom с открытым исходным кодом, рои ИИ-агентов за 24 дня создали около 43,1 миллиона строк кода на Lean, охватив 715 статей и книг и выявив 34 расхождения с опубликованными материалами. В публикации новостного аккаунта об ИИ TestingCatalog добавляется, что агенты разделили работу как команды разработчиков ПО и писали код быстрее, чем Lean успевал его проверять.

Эти цифры приводятся самой Axiom; независимая проверка формализации в объявлении не упоминается. К 28 октября публикация набрала около 6 200 лайков в X.