Time：9:00-11:00, 14:00-16:00, January 2-19, 2024
Venue: TBD
Organizer：Professor Huayi Chen
Speaker: Jiedong Jiang, Peking University
Registration:
For Westlake University students: please scan the QR code to register
For students outside the Westlake University: click the link to register: https://www.wjx.cn/vm/OFwSwTv.aspx#
Introduction to Lean: Lean is an interactive theorem prover and a programming language that can be used to check the reliability of mathematical proofs. Its theoretical foundation is based on dependent type theory. It was initially launched by Leonardo de Moura and others in 2013 at Microsoft Research. Lean also has an accompanying mathematical theorem library called Mathlib. As of March 2023, Mathlib contains over 110,000 theorems and 1,100,000 lines of code. In 2018, Kevin Buzzard and others used Lean in the Liquid tensor experiment to verify a series of theorems about condensed mathematics by Fields Medalist Peter Scholze.
Course Outline: This course aims to introduce students with a certain mathematical background to the interactive theorem proving language Lean. It is hoped that students will master the common proof tactics (i.e., proof syntax) of Lean and the ability to formalize known mathematical theorems using Lean. After an overall introduction, the course plans to introduce related common tactics and other functions in special topics. The specific plan is as follows:
1. Installation and ontroduction of Lean (If time permits, introduction of type theory)
2. Natural Number Games
3. Basic grammar of 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
Note: The specific arrangements depend on the teaching progress. Each topic comes with exercises, and students are expected to complete these exercises after class to achieve better learning outcomes. It is recommended that students preview the definitions of groups, rings, and fields in abstract algebra, as well as the definition of topological spaces. Additionally, it is best to bring a laptop to facilitate completing the course exercises.
References：
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/
Further readings：https://leanprover-community.github.io
