[开源] 使用Lean定理证明器重写《数学原理》：罗素经典著作的现代化尝试
talkingdev • 2025-04-25
5689 views
近日，开发者ndrwnaguib在GitHub上发布了一个引人注目的开源项目，旨在使用Lean4定理证明器对伯特兰·罗素教授的经典著作《数学原理》第一卷进行形式化验证。该项目严格遵循罗素原著中的证明过程，仅在必要时添加形式化所需的辅助陈述，力求保持原作的逻辑严谨性。作者特别强调，欢迎发现任何不准确之处的反馈，以延续数学基础研究的精确传统。值得注意的是，此前已有学者使用Rocq（原Coq）对《数学原理》进行过形式化验证，但该项目选择Lean4作为工具链，既是对新兴证明助手的实践探索，也展现了形式化数学工具的多样性发展。该项目不仅为数学基础研究提供了数字化范本，更推动了定理证明器在数学哲学领域的应用边界。
核心要点
- 使用Lean4定理证明器对罗素《数学原理》进行完整形式化验证
- 严格遵循原著证明逻辑，仅在形式化必要处添加辅助陈述
- 项目延续了Elkind等人使用Rocq的形式化传统，但采用新兴的Lean4工具链