Редакция VseTime.ru сообщает:
Компания Axiom Math сообщила о завершении компьютерной формализации теоремы классификации конечных простых групп, или «Огромной теоремы» — одного из крупнейших достижений математики XX века. Теорема [note=6469|классифицирует] конечные простые математические группы — базовые элементы, из которых можно составить любую конечную группу, подобно тому, как сложные числа раскладываются на простые множители. Работа над ее доказательством длится уже более полувека. В 1963 году американские математики Уолтер Фейт (Walter Feit) и Джон Томпсон (John Griggs Thompson) [note=6468|доказали], что порядок любой неабелевой конечной простой группы четен. Завершить классификацию в 1983 году смог Дэниел Горенстайн (Daniel Gorenstein), а в 2004 году Майкл Ашбахер (Michael Aschbacher) и Стивен Смит (Stephen D. Smith) опубликовали изложение объемом в 1221 страницу, завершив тем самым то, что стало известно как доказательство первого поколения. Именно его формализацией и занималась Axiom Math.
Источник: https://nplus1.ru/news/2026/10/28/big-math-ai