课程时间：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
