课程时间：2024年1月2日至1月19日，每天09:00-11:00,14:00-16:00
地点：待定
组织者：陈华一教授
主讲人：北京大学 姜杰东
报名方式：
校内学生：扫描二维码，用学校邮箱登录后进行报名
校外学生：请点击链接进行报名:https://www.wjx.cn/vm/OFwSwTv.aspx#
Lean简介：Lean是一款交互式定理证明器，也是一门编程语言，可用于检验数学证明的可靠性，其理论基础基于依赖类型论（dependent type theory）。最初由Leonardo de Moura等人于2013年在微软研究院推出。 Lean同时拥有一个与之配套的数学定理库，称为Mathlib。 截止至2023年3月，Mathlib 已经包含了超过110,000个定理和1,100,000行代码。2018年，Kevin Buzzard等人曾在Liquid tensor experiment中使用Lean验证菲尔兹奖得主Peter Scholze关于凝聚态数学的一系列定理。
课程纲要：本课程旨在向具有一定数学背景的学生介绍交互式定理证明语言Lean。希望与课同学能掌握Lean的常用证明tactic（即证明语法），掌握使用Lean形式化已知数学定理的能力。课程计划在进行整体简介后，分专题介绍相关的常用tactic及其他功能。具体计划如下:
1. Lean安装及简介（如有时间+类型论简介）
2. Natural Number Games
3. Lean语法基础
4. Logic
5. Sets and Functions
6. Elementary Number Theory
7. Structures
8. Hierarchies
9. Groups and Rings
10. Topology
11. Differential Calculus
12. Integration and Measure Theory
备注：具体安排视教学进度而定。每个专题都附有练习，需要与课同学完成课后练习以达到更好的学习效果。建议同学预习抽象代数中群、环、域的定义，以及拓扑空间的定义。另外，最好携带笔记本电脑以方便完成课程练习。
主要教材及练习请参考：
1. （Natural Number Games）https://adam.math.hhu.de/#/g/hhu-adam/NNG4
2. （Mathematics in Lean）https://leanprover-community.github.io/mathematics_in_lean/
更多材料可参考：https://leanprover-community.github.io
