如今，AI 已经能为相当一部分数学命题生成可由 Lean 检查的形式化证明。证明由一个很小的内核逐步检查，因而不必相信；但证明针对的那个命题是不是数学家心中的命题，没有机器能够担保。近年公开的形式化项目中，不少错误正是出在命题本身：一个被排除错了的变量，一条默认而未写出的假设，或者一个在定义域之外取约定值的函数。

本课程以 Lean 4 与 Mathlib 为对象，讨论怎样把数学准确地写成形式语言：Mathlib 如何表示数系、代数结构、线性代数、极限与拓扑等常见对象；约定值、类型转换与量词次序怎样悄悄改变命题的含义；怎样借助小证明和检查工具判断一个命题是否写对；以及怎样把一个大证明拆成若干中间命题，写出把它们串联起来的证明骨架，再把各个部分分别交给 AI 或他人完成。

每次课分为四个单元。第一单元讲形式化数学的故事与背景；第二、三单元通过现场演示讲解技术内容；第四单元介绍类型论、Curry–Howard 对应以及 Lean 背后的程序语言原理。课程面向对形式化感兴趣的数学工作者，不要求编程经验。