我们介绍了一种基于依赖类型的证明器，旨在模拟 LLM（大语言模型）和人类书写数学的方式，补充现有的系统如 Lean 和 Coq。其核心设计选择包括一种模仿数学自然语言的表面结构，以及一个规则驱动的自动化层，能够完成教科书中常常省略的常规步骤，从而使得接受的证明能够重新输出为经过检查的 Lean 文件。
早期实验表明，即使没有任何特定于证明器的训练数据，LLM 也能在 miniF2F 基准上有效地学习使用该证明器。
Lean 输出摘录可见于 GitHub。
博主点评： 该项目通过将 LLM 的自然语言处理能力与形式化证明结合，为数学证明的自动化开辟了新路径。其设计的自然语言表面和自动化规则显著降低了用户的学习成本，值得关注。