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

Компания Axiom Math объявила о завершении компьютерной формализации теоремы классификации конечных простых групп. Её называют «Огромной теоремой» и относят к главным результатам математики XX века.

Теорема описывает конечные простые группы — базовые элементы, из которых строится любая конечная группа. Аналогия привычная: как целое число раскладывается на простые множители, так и конечная группа собирается из простых. Доказательство этого утверждения занимало математиков более полувека.

В 1963 году американские математики Уолтер Фейт (Walter Feit) и Джон Томпсон (John Griggs Thompson) доказали, что порядок любой неабелевой конечной простой группы чётен. Классификацию в 1983 году завершил Дэниел Горенстайн (Daniel Gorenstein). В 2004 году Майкл Ашбахер (Michael Aschbacher) и Стивен Смит (Stephen D. Smith) выпустили изложение объёмом 1221 страница — оно известно как доказательство первого поколения. Формализацией именно этого текста и занималась Axiom Math.

Компьютерная формализация означает перевод доказательства на язык, который проверяет программа. Такая запись не оставляет места для пропущенных случаев и нестрогих переходов, на которые обычно опирается изложение на бумаге.