Formalising published mathematics

前置知识

22 项必需的前置知识（一直追溯到底）

你将学会

• Write a blueprint that breaks a published theorem into formalisable lemmas and records their dependencies.
• Formalise a short published result, recording any gaps or implicit assumptions found along the way.
• Describe completed large formalisations and what they did and did not verify.

定义

• A blueprint is a document linking each informal definition and lemma to its formal counterpart and recording the dependencies between them.
• The trusted base of a formal proof is what must be trusted for the check to be meaningful: the proof checker's kernel, the axioms used and the formal statement.

定理

• The Liquid Tensor Experiment formalised a central theorem of Clausen and Scholze's condensed mathematics in Lean; it was completed in 2022.
• The Feit–Thompson odd order theorem was formalised in Coq by Gonthier and collaborators (2012).
• Formalisation verifies the proof of the formal statement; whether that statement faithfully captures the published theorem must be checked by people.

常见误解

• Thinking formalisation makes peer review unnecessary.
• Believing a formal proof follows the informal paper line by line; formal proofs often reorganise the argument substantially.

可选发现

• ← Mathematical writing
• ← Computational reproducibility

学习路径

• Research preparation

延伸阅读

• Jeremy Avigad and Patrick Massot, Mathematics in Lean
• Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4