What's new by TerryTao
·
《Analysis I》的Lean伴侣
💡
原文英文，约700词，阅读约需3分钟。
📝
内容提要
作者计划为20年前的实分析教材《Analysis I》推出Lean伴侣，将书中的定义、定理和习题转化为Lean代码，以便于使用证明助手进行验证。该伴侣将逐步依赖Mathlib库，帮助学生在学习实分析的同时掌握Lean编程。
🎯
关键要点
- 作者计划为20年前的实分析教材《Analysis I》推出Lean伴侣，将书中的内容转化为Lean代码。
- 该伴侣旨在帮助学生在学习实分析的同时掌握Lean编程。
- Lean伴侣将包含书中的定义、定理和习题的翻译，提供替代的练习方式。
- 目前，教材的某些章节已被翻译为Lean，部分内容依赖于Mathlib库。
- 作者计划在书中逐步增加对Mathlib定义和函数的依赖，作为Lean和Mathlib的入门。
- 该伴侣的代码已在Lean中编译，但尚未测试所有的“sorries”是否可以被填充。
- 作者欢迎志愿者进行“试玩”，以验证伴侣的可行性和提供反馈。
❓
延伸问答
《Analysis I》的Lean伴侣有什么目的？
Lean伴侣旨在将《Analysis I》中的定义、定理和习题转化为Lean代码，帮助学生在学习实分析的同时掌握Lean编程。
Lean伴侣如何帮助学生进行练习？
学生可以通过在Lean代码中填充对应的“sorries”来完成书中的习题，从而以另一种方式进行练习。
Lean伴侣依赖于哪些库？
Lean伴侣部分依赖于Mathlib库，以便在学习过程中逐步引入其定义和函数。
目前Lean伴侣的开发进展如何？
目前，教材的某些章节已被翻译为Lean，代码已在Lean中编译，但尚未测试所有的“sorries”是否可以被填充。
作者对志愿者的期望是什么？
作者欢迎志愿者进行“试玩”，以验证伴侣的可行性并提供反馈。
Lean伴侣与《Analysis I》的关系是什么？
Lean伴侣是对《Analysis I》中内容的翻译，旨在为学习者提供一种新的学习和验证方式。
➡️
