Вышла новая статья по формализации КТП, в которой утверждается, что КТП формализована с использованием Lean/Mathlib. Я старался избегать траты времени на горячие темы ИИ и доказательства теорем, но в данном случае есть много...