In this paper we present a new "external verifier" for the Lean theorem prover, written in Lean itself. This is the first complete verifier for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new verifier 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 verifier 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 show that the kernel correctly implements this theory, to eliminate the possibility of implementation bugs in the kernel and increase the trustworthiness of proofs conducted in it. This work is still ongoing but 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在自主托管完整阐述器与编译器方向迈出了新的一步。此外，由于该验证器采用支持形式化验证的语言编写，可对核心本身进行性质描述与证明。我们报告了在此方向上的初步进展：对Lean类型理论进行抽象形式化，并证明验证器正确实现了该理论，从而消除核心实现中的潜在错误，提升基于该核心所完成证明的可信度。尽管本工作仍在进行中，我们计划通过此项目论证未来对核心与类型理论的任何修改，确保抽象理论或实现错误不会引入非安全性问题。