Компания Axiom Math объявила об успешном завершении компьютерной формализации теоремы классификации конечных простых групп, которую также называют «Огромной теоремой». Это достижение считается одним из наиболее значимых успехов в области математики XX века.
Данная теорема занимается классификацией конечных простых математических групп, которые являются фундаментальными строительными блоками для формирования любых конечных групп, аналогично тому, как сложные числа делятся на простые множители.
Работа над доказательством этой теоремы продолжалась на протяжении более чем половины столетия. Первые шаги были сделаны в 1963 году, когда американские математики Уолтер Фейт и Джон Томпсон доказали, что порядок любой неабелевой конечной простой группы является четным.
Классификация была окончательно завершена в 1983 году Дэниелом Горенстайном. Более того, в 2004 году Майкл Ашбахер и Стивен Смит опубликовали изложение, насчитывающее 1221 страницу, что ознаменовало собой завершение так называемого доказательства первого поколения. Именно эту работу взяла на себя формализация компании Axiom Math.