Компьютерное доказательство теории конденсированной математики — первый шаг к «великому объединению»
Пример расчётного доказательства в Lean Математики давно используют компьютеры в своей работе как инструменты для сложных вычислений и выполнения рутинных операций перебора. Например, в 1976 году методом компьютерного перебора была доказана теорема о четырёх красках. Это была первая крупная теорема, доказанная с помощью компьютера. Теперь вспомогательный софт для доказательства теорем (proof assistant software) не просто...