Lean 4 定理证明器综合调查：架构、应用与进展
计算机科学中的逻辑
2025-02-03 v1 编程语言
摘要
本综合调查 examines Lean 4，这是一种领先的交互式定理证明器和函数式编程语言。我们分析了其架构设计、类型系统、元编程能力以及在形式化验证和数学中的实际应用。通过与其他证明助理的详细比较和广泛的案例研究，我们展示了Lean 4在证明自动化、性能和可用性方面的独特优势。该文还探讨了其生态系统的最新发展，包括库、工具和教育应用，为Lean 4在形式方法和数学形式化方面日益增长的影响提供了见解。
引用
@article{arxiv.2501.18639,
title = {A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances},
author = {Xichen Tang},
journal= {arXiv preprint arXiv:2501.18639},
year = {2025}
}