In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean's mathlib library, forming an additional step in Lean's aim to self-host the full elaborator and compiler. Moreover, because the checker is written in a language which admits formal verification, it is possible to state and prove properties about the kernel itself, and we report on some initial steps taken in this direction to formalize the Lean type theory abstractly and express the relation between the kernel functions and the type theory. We plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs.

翻译：本文提出了一种为 Lean 定理证明器开发的新型“外部检查器”，该检查器完全使用 Lean 语言自身编写。这是除 Lean 自身使用的 C++ 参考实现外，首个完整的 Lean 4 类型检查器。我们的新检查器性能与原版相当，运行速度慢 20% 至 50%，可用于验证 Lean 的整个 mathlib 库，为实现 Lean 自托管完整 elaborator 和编译器的目标迈出了重要一步。此外，由于该检查器采用支持形式化验证的语言编写，我们能够陈述并证明关于内核自身的性质。本文报告了在此方向上的一些初步进展，包括对 Lean 类型论进行抽象形式化，以及表达内核函数与类型论之间的关系。我们计划利用此项目来论证未来对内核及类型论的任何修改，并确保无论是抽象理论还是实现缺陷都不会引入不一致性。