Introduction to Lean for Programmers
Introduction to Lean for Programmers
程序员的 Lean 入门指南
Programming Introduction to Lean for Programmers: The syntax and semantics of mathematics 程序员的 Lean 编程入门：数学的语法与语义
Ronen Lahat | May 19, 2026 | 15 min read Ronen Lahat | 2026年5月19日 | 15分钟阅读
Intro to proof assistants 证明助手简介
I’m a software engineer who transitioned into data science, and I work daily with machine learning algorithms. I’m fascinated both by their apparent magic and by the mathematics that underlies them. Pry open any machine learning library and you’ll find mathematical tricks involving matrix decompositions, convolutions, Gaussian curves, and more. These, in turn, are built on even more fundamental axioms and rules, such as function application and logic. 我是一名转型为数据科学家的软件工程师，每天都在与机器学习算法打交道。我既被它们看似神奇的表现所吸引，也对支撑它们的数学原理着迷。拆开任何一个机器学习库，你都会发现涉及矩阵分解、卷积、高斯曲线等数学技巧。而这些技巧，又建立在函数应用和逻辑等更基础的公理和规则之上。
During my journey to learn these primitives, I collected a whole shelf of mathematics books, many of which now gather dust. I also enrolled at the Open University, where I attended classes over Zoom and learned about syntax and axioms, then how to combine them to build theorems. The topic was fascinating: axioms are like game pieces and legal moves on a board, while theorems are legal plays, some more interesting than others. Proving a theorem means unwinding the gameplay just enough to convince the players that it is reachable, or disproving it by pointing out an impossibility. For example: “The two bishops are on white squares, and a bishop can never switch to a square of a different color.” 在学习这些基础知识的过程中，我收集了一书架的数学书，其中许多现在都已落满灰尘。我还报名参加了开放大学的课程，通过 Zoom 上课，学习语法和公理，以及如何将它们组合起来构建定理。这个主题非常迷人：公理就像棋盘上的棋子和合规的走法，而定理则是合法的对局，有些比其他的更有趣。证明一个定理意味着将游戏过程推演到足以让参与者相信它是可达的，或者通过指出某种不可能的情况来反驳它。例如：“两枚象都在白格上，而象永远无法移动到不同颜色的格子上。”
But on a practical level, the courses were tedious. I was given PDFs to solve by hand and then submit scans of my work online. While scribbling with pencil on paper, struggling with the course assignments I had two insights: Building a proof is like programming. There’s no way I can engage with mathematics in these early century conditions. I need an IDE, with type hints, syntax highlighting, and descriptive error messages, and engage with it interactively. My thoughts weren’t new. The first idea is called the Curry-Howard correspondence, explained below. The latter is the goal of proof assistants such as Lean and their IDE extensions (usually a VS Code extension). 但在实践层面，这些课程非常枯燥。我需要手动完成 PDF 习题，然后将作业扫描件提交到网上。在纸上用铅笔涂写、为课程作业挣扎时，我有了两个洞见：构建证明就像编程；我无法在这种“上世纪”的条件下进行数学研究。我需要一个带有类型提示、语法高亮和描述性错误信息的 IDE，并能以交互方式进行工作。我的想法并不新鲜。第一个想法被称为“柯里-霍华德同构”（Curry-Howard correspondence），下文会解释。后者正是 Lean 等证明助手及其 IDE 扩展（通常是 VS Code 扩展）的目标。
Interactive proof assistants vs automatic theorem provers 交互式证明助手与自动定理证明器
Theorem checkers like Lean’s kernel can determine whether expressions are well-formed, if the steps are legal, and if the final conclusion is valid. Interactive proof assistants build on them and will also help you build your proofs and suggest steps. Automatic theorem provers (ATPs) attempt to find the proof on their own using AI techniques. Lean works as a proof checker and assistant, but it pairs well with generative AI to function effectively as an ATP. 像 Lean 内核这样的定理检查器可以确定表达式是否格式良好、步骤是否合法以及最终结论是否有效。交互式证明助手建立在它们之上，还会帮助你构建证明并建议步骤。自动定理证明器（ATPs）则尝试利用人工智能技术自行寻找证明。Lean 既是证明检查器也是助手，但它与生成式 AI 结合得很好，可以有效地作为自动定理证明器使用。
Terence Tao streams AI-assisted proofs on his YouTube channel using Lean 4 and GitHub Copilot. Most of the headlines in the form of “AI just solved an x-years-old open problem” were likely formalized with Lean (example 1, example 2, and 3). AI projects and benchmarks such as LeanDojo, miniF2F, ProofNet, PutnamBench, FormalMATH, use Lean. OpenAI and Meta have trained models to use Lean, and DeepMind’s AlphaProof used it to earn a silver medalist at the International Mathematical Olympiad. 陶哲轩（Terence Tao）在他的 YouTube 频道上使用 Lean 4 和 GitHub Copilot 直播 AI 辅助证明的过程。大多数标题为“AI 刚刚解决了困扰 x 年的开放性问题”的新闻，很可能都是用 Lean 形式化验证的（示例 1、示例 2 和 3）。LeanDojo、miniF2F、ProofNet、PutnamBench、FormalMATH 等 AI 项目和基准测试都在使用 Lean。OpenAI 和 Meta 已经训练了使用 Lean 的模型，而 DeepMind 的 AlphaProof 则利用它在国际数学奥林匹克竞赛中获得了银牌水平。
The Curry-Howard correspondence 柯里-霍华德同构
Let’s start with a simple logic theorem, something you might have to prove in an undergraduate logic class: (P → Q → R) → (P ∧ Q → R). The operator → denotes logical implication, but in the Curry-Howard correspondence between proofs and computer programs it can be read as a function. ∧ is the logical “and.” In plain English, we’re asking whether this statement is true: “If I have a function that, given P, produces a function from Q to R, then if I already have both P and Q already, I can produce R.” 让我们从一个简单的逻辑定理开始，这可能是你在本科逻辑课上需要证明的内容：(P → Q → R) → (P ∧ Q → R)。运算符 → 表示逻辑蕴含，但在证明与计算机程序之间的柯里-霍华德同构中，它可以被解读为一个函数。∧ 是逻辑“与”。用通俗的话说，我们是在问这个陈述是否为真：“如果我有一个函数，给定 P 后能产生一个从 Q 到 R 的函数，那么如果我已经同时拥有 P 和 Q，我就能产生 R。”
Note: (P → Q → R) is a “curried function,” (Haskell Curry is here to blame as well), and the syntax is equivalent to (P → (Q → R)). In programming terms, it’s a function that returns another function, which can later be invoked as foo(bar)(baz). It’s logically equivalent to foo receiving both bar and baz as a tuple foo((bar, baz)), but that is what we’re trying to prove here. Likewise, the entire sentence could be written as (P → Q → R) → P ∧ Q → R. 注意：(P → Q → R) 是一个“柯里化函数”（Haskell Curry 也难辞其咎），其语法等同于 (P → (Q → R))。在编程术语中，这是一个返回另一个函数的函数，稍后可以像 foo(bar)(baz) 那样调用。它在逻辑上等同于 foo 同时接收 bar 和 baz 作为元组 foo((bar, baz))，但这正是我们试图证明的内容。同样，整个句子可以写成 (P → Q → R) → P ∧ Q → R。
If you were told to prove that this is possible as a programmer, you might be tempted to do so by writing a function that conforms to this scenario. In TypeScript we might write: 如果有人让你以程序员的身份证明这是可能的，你可能会尝试编写一个符合此场景的函数。在 TypeScript 中，我们可以这样写：
function prove<P, Q, R>(f: (p: P) => (q: Q) => R): (pq: [P, Q]) => R {
return ([p, q]) => f(p)(q);
}We defined a function — our theorem — that receives a curried function (P → Q → R) as a parameter and outputs a function that receives a product type P ∧ Q and outputs R, that is, (P ∧ Q → R). This function acts as a “witness” that the logic theorem is true. The proof looks sound and it even satisfies the types that spell the original theorem in TypeScript. 我们定义了一个函数——即我们的定理——它接收一个柯里化函数 (P → Q → R) 作为参数，并输出一个接收乘积类型 P ∧ Q 并输出 R 的函数，即 (P ∧ Q → R)。这个函数充当了逻辑定理为真的“见证者”。这个证明看起来很稳健，它甚至满足了 TypeScript 中拼写出原始定理的类型。