Классификацию конечных простых групп полностью формализовали в Lean

Classification of Finite Simple Groups Formalized in Lean

Первое поколение доказательства классификации конечных простых групп занимает тысячи журнальных страниц и создавалось около сотни математиков десятилетиями. Теперь команда Axiom Math представила полную формализацию этого доказательства на Lean: 43,1 млн строк кода, 2,05 млн деклараций и 100 ключевых этапов, каждый логический шаг проверен ядром Lean. В процессе авторы обнаружили ошибку в опубликованном аргументе для теоремы о несбалансированных группах и предложили альтернативный путь доказательства.