Lean中的数学形式化
如今，AI 已经能为相当一部分数学命题生成可由 Lean 检查的形式化证明。证明由一个很小的内核逐步检查，因而不必相信；但证明针对的那个命题是不是数学家心中的命题，没有机器能够担保。近年公开的形式化项目中，不少错误正是出在命题本身：一个被排除错了的变量，一条默认而未写出的假设，或者一个在定义域之外取约定值的函数。
本课程以 Lean 4 与 Mathlib 为对象，讨论怎样把数学准确地写成形式语言：Mathlib 如何表示数系、代数结构、线性代数、极限与拓扑等常见对象；约定值、类型转换与量词次序怎样悄悄改变命题的含义；怎样借助小证明和检查工具判断一个命题是否写对；以及怎样把一个大证明拆成若干中间命题，写出把它们串联起来的证明骨架，再把各个部分分别交给 AI 或他人完成。
每次课分为四个单元。第一单元讲形式化数学的故事与背景；第二、三单元通过现场演示讲解技术内容；第四单元介绍类型论、Curry–Howard 对应以及 Lean 背后的程序语言原理。课程面向对形式化感兴趣的数学工作者，不要求编程经验。
本课程以 Lean 4 与 Mathlib 为对象，讨论怎样把数学准确地写成形式语言：Mathlib 如何表示数系、代数结构、线性代数、极限与拓扑等常见对象；约定值、类型转换与量词次序怎样悄悄改变命题的含义；怎样借助小证明和检查工具判断一个命题是否写对；以及怎样把一个大证明拆成若干中间命题，写出把它们串联起来的证明骨架，再把各个部分分别交给 AI 或他人完成。
每次课分为四个单元。第一单元讲形式化数学的故事与背景；第二、三单元通过现场演示讲解技术内容；第四单元介绍类型论、Curry–Howard 对应以及 Lean 背后的程序语言原理。课程面向对形式化感兴趣的数学工作者，不要求编程经验。
Lecturer
Date
26th October, 2026 ~ 11th January, 2027
Location
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| Monday | 14:20 - 17:50 | A3-2a-302 | Tencent A | 482 969 7386 | 106457 |
Audience
Graduate
, Advanced Undergraduate
, Postdoc
, Researcher
Video Public
No
Notes Public
No
Language
Chinese
Lecturer Intro
Hanru Jiang is an Associate Researcher at BIMSA. He received his Ph.D. in Computer Science and Technology from the University of Science and Technology of China in 2019. From 2019 to 2020, he was an Assistant Researcher at the Quantum Computing Research Center, Peng Cheng Laboratory. His research interests lie in programming language theory, formal verification of compilers, and programming language issues in quantum computing. His work has been published in premier venues such as PLDI, CAV, and OOPSLA. He was a recipient of the PLDI 2019 Distinguished Paper Award.