这两天挺火的Lean语言是一个编程语言和定理证明器。最新版本Lean 4 的目标是提供一个高效、可扩展、可靠的平台，用于形式化数学、验证软件和硬件，以及开发通用的函数式程序。

现在局势已然明了，它或某个取代它的后继语言，代表着数学论文写作的未来。

这里提供一本关于Lean的英语手册

http://t.cn/A6lLTF5C