Как устроены новые системы решения математических задач?

Пользователь спрашивает о принципах работы новых систем, решающих математические задачи: они генерируют утверждения в LEAN, проверяют их компилятором и постепенно собирают доказательство. Автор хочет создать собственную упрощенную версию для задачи по многомерной геометрии и интересуется практическими деталями реализации.