用Lean证明分析I：一个交互式学习项目
2025-05-31
作者将自己20年前的实分析教材《分析I》用Lean证明助手进行了形式化。这个项目并非简单的翻译，而是将书中的定义、定理和习题转化为Lean代码，读者可以通过填补代码中的“sorries”来完成习题，并逐步学习Lean和Mathlib数学库。项目目前已完成部分章节的转换，并设计了从“手工”构建自然数到使用Mathlib标准库的过渡，方便学习者逐步掌握。作者邀请志愿者参与测试和完善项目。
开发
实分析