Часть 3 из 3

Классификация остаётся достижением создавших её математиков. Проект использовал Lean, Mathlib и около 1,2 млн строк из Qiuzhen-CFSG. В публикации формализации доступны итоговая теорема, инструкции проверки и промежуточные результаты. Работа над исправлениями продолжается со специалистами, включая Лайонса и Соломона. Заявленная формализация позволяет проверять условия и зависимости огромного доказательства как единое целое и использовать его части в дальнейшей математике.

Наши каналы
MAX · Telegram · Дзен

#ТеорияГрупп #Симметрия #Формализация #Доказательства