Axiom Math завершила компьютерную формализацию доказательства теоремы классификации конечных простых групп, известной как «Огромная теорема». Она классифицирует конечные простые группы — базовые элементы, из которых можно составить любую конечную группу.

Работа над доказательством теоремы продолжалась более полувека. В 1983 году Дэниел Горенстайн завершил классификацию, а в 2004 году Майкл Ашбахер и Стивен Смит опубликовали изложение доказательства первого поколения объемом 1221 страницу. Именно это доказательство формализовала компания.

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