一种看起来非常值得尝试制作的“高级编程语言”，是一种可以被编译成 Lean（或 HOL，或其他）的语言，专注于让人类尽可能容易地阅读定义和定理。 不是证明——因为对于证明来说，唯一重要的是证明是正确的——而是定义和定理。 预期的使用场景是，AI 输出了一堆证明，而你试图让任何阅读输出的人尽可能容易地理解那些已经被证明的实际精确主张是什么。