《Analysis I》的Lean伴侣
原文英文，约700词，阅读约需3分钟。
📝
内容提要
作者计划为20年前的实分析教材《Analysis I》推出Lean伴侣，将书中的定义、定理和习题转化为Lean代码，以便于使用证明助手进行验证。该伴侣将逐步依赖Mathlib库，帮助学生在学习实分析的同时掌握Lean编程。
🔎
延伸解读
Lean伴侣的学习价值
Lean伴侣不仅是对《Analysis I》的内容转化，更是学生学习实分析和Lean编程的桥梁。通过将定义和定理转化为代码，学生可以在实践中加深对理论的理解，提升逻辑思维能力。
与Mathlib的关系
Lean伴侣的设计逐步依赖于Mathlib库，这意味着学生在学习过程中将接触到更广泛的数学工具和概念。随着学习的深入，学生将逐渐从基础的定义过渡到使用Mathlib的高级功能，增强了学习的连贯性。
参与测试的机会
作者欢迎志愿者参与Lean伴侣的测试，这不仅是对伴侣可行性的验证，也是学习Lean编程的良机。参与者可以通过解决“sorries”来提升自己的编程能力，同时为项目提供宝贵反馈。
❓
Q&A
《Analysis I》的Lean伴侣有什么目的？
Lean伴侣旨在将《Analysis I》中的定义、定理和习题转化为Lean代码，帮助学生在学习实分析的同时掌握Lean编程。
Lean伴侣如何帮助学生进行练习？
学生可以通过在Lean代码中填充对应的“sorries”来完成书中的习题，从而以另一种方式进行练习。
Lean伴侣依赖于哪些库？
Lean伴侣部分依赖于Mathlib库，以便在学习过程中逐步引入其定义和函数。
目前Lean伴侣的开发进展如何？
目前，教材的某些章节已被翻译为Lean，代码已在Lean中编译，但尚未测试所有的“sorries”是否可以被填充。
作者对志愿者的期望是什么？
作者欢迎志愿者进行“试玩”，以验证伴侣的可行性并提供反馈。
Lean伴侣与《Analysis I》的关系是什么？
Lean伴侣是对《Analysis I》中内容的翻译，旨在为学习者提供一种新的学习和验证方式。
🏷️
