Для этого потребовалось около 43,1 миллиона строк кода Компания Axiom Math сообщила о завершении компьютерной формализации теоремы классификации конечных простых групп, или «Огромной теоремы» — одного из крупнейших достижений математики XX века. Теорема Исходное доказательство «Огромной теоремы» занимает около 15 тысяч страниц в более чем 500 научных статьях, написанных примерно сотней математиков. Их статья объемом 255 страниц заняла целый выпус
