Axiom Math за 24 дня проверила машиной доказательство, которое писали десятилетиями

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

Формализация означает, что всё доказательство переписано на Lean и проверено машиной — каждый шаг либо выводится из предыдущих, либо отвергается. До сих пор полноты этого доказательства никто не мог гарантировать: его не держал в голове ни один человек.

Результат опубликован отдельным сайтом с исходниками формализации.