从零到QED：用Lean 4进行非正式的形式化介绍

从零到QED：用Lean 4进行非正式的形式化介绍
From Zero to QED: An informal introduction to formality with Lean 4

原始链接: https://sdiehl.github.io/zero-to-qed/01_introduction.html

《从零到QED》是一个学习系列，旨在从基础开始教授Lean 4，这是一种功能强大但目前文档不足的形式化语言。该资源力求弥补现有学习材料的不足，采用实用、非正式的方法。该系列分为两部分：第一部分是Lean作为一种编程语言，涵盖语法、类型以及单子和IO等编程概念；第二部分是Lean作为定理证明器，深入探讨证明写作、类型论和策略。值得注意的是，整个系列*本身*就是一个Lean项目——所有代码和证明都经过机器验证，并可在GitHub上获取（github.com/sdiehl/zero-to-qed）。无需先前的定理证明经验，但熟悉函数式编程会有所帮助。该系列以探讨形式化方法在人工智能时代日益增长的相关性作为结尾。它是一个实用的入门点，与更严谨的学术资源形成对比。

## 从零到QED：LLM与数学证明的未来一项新资源（[sdiehl.github.io/zero-to-qed/](https://sdiehl.github.io/zero-to-qed/)）介绍了使用Lean 4进行形式化数学证明，引发了Hacker News上的讨论。对话的中心是大型语言模型（LLM）可能如何影响该领域，特别是随着证明变得越来越复杂——可能超过人类验证的能力。一个关键的担忧是，数学家是否能够自信地验证由LLM生成的数百万行代码的证明。虽然Lean编译器确保了*形式化*的正确性，但信任可能会从人类理解转移到对工具链本身的依赖。一些人认为，证明的核心价值不仅在于真理，还在于在过程中发展理解和新的数学思想。另一些人指出，Lean的受信任内核足够小，可以供人类审查，并强调模块化、"美观"证明的重要性，这些证明仍然易于理解。一个主要的争论点在于形式化是阻碍还是增强了数学探索，一些数学家对采用额外的工作犹豫不决。然而，像Kevin Buzzard这样的倡导者展示了对证明助手日益增长的参与度。

Welcome to From Zero to QED, an informal introduction to formality in Lean 4. This article series teaches the language from first principles. Lean is expressive but the learning resources remain scattered and incomplete. This series is a best effort to fill that gap.

Note

This is the beta release. There are bound to be typos, errors, and rough edges. If you spot something, send a PR on GitHub.

Tip

This article series is itself a Lean project. Every code sample, every proof, every theorem is extracted from source files that the Lean compiler typechecks on every build. The text you are reading is backed by machine-verified code in the GitHub repository. Call it a literate proof.

The series divides into two arcs. The first arc treats Lean as a programming language. You will learn the syntax, type system, control flow, polymorphism, monads, and IO. By the end of this arc you can write real programs in Lean.

The second arc treats Lean as a theorem prover. You will learn to write proofs, understand type theory and dependent types, master tactics, and eventually prove classic mathematical results. The series concludes with the emerging intersection of theorem proving with artificial intelligence, and why formal methods may matter more in the coming decade than they have in the previous five.

No prior experience with theorem provers is assumed. Familiarity with a typed functional language like Haskell, OCaml, or Scala helps but is not required.

The full source code is available on GitHub: github.com/sdiehl/zero-to-qed

To run the examples locally, install Lean 4 and clone the repository:

git clone https://github.com/sdiehl/zero-to-qed
cd zero-to-qed
lake build

You can also serve the documentation locally with just serve if you have mdBook installed.

Additional learning resources are collected in the References appendix. This series is an informal introduction to formality. If you want the stuffy formal introduction to formality, see Theorem Proving in Lean 4, Functional Programming in Lean, Mathematics in Lean, or university courses from CMU, Imperial, and Brown. They are more rigorous.

从零到QED：用Lean 4进行非正式的形式化介绍 From Zero to QED: An informal introduction to formality with Lean 4

从零到QED：用Lean 4进行非正式的形式化介绍
From Zero to QED: An informal introduction to formality with Lean 4