Formalising published mathematics

Lens

MotivationH

One sentence, and a challenge

In 1990 Don Zagier published in the American Mathematical Monthly a paper whose entire mathematical content is one sentence:

The involution on the finite set $S = \{(x, y, z) \in \N^3 : x^2 + 4yz = p\}$ defined by
$(x, y, z) \mapsto \begin{cases} (x + 2z,\; z,\; y - x - z) & \text{if } x < y - z, \\ (2y - x,\; y,\; x - y + z) & \text{if } y - z < x < 2y, \\ (x - 2y,\; x - y + z,\; y) & \text{if } x > 2y \end{cases}$
has exactly one fixed point, so $|S|$ is odd and the involution defined by $(x, y, z) \mapsto (x, z, y)$ also has a fixed point.

That sentence proves Fermat's theorem: every prime $p \equiv 1 \pmod 4$ is a sum of two squares. An expert reads it in a minute and checks it in ten. What would it take to convince a computer — a proof checker that knows nothing except the rules of logic and the definitions we give it? Every word must be justified: "the finite set", "involution", "exactly one", "so". This lesson does that, completely, and keeps a list of everything the sentence leaves unsaid.

At the other end of the scale, in December 2020 Peter Scholze challenged the community to formalise a central theorem of the condensed mathematics he had developed with Dustin Clausen, saying that he was not fully confident that every detail of its intricate proof was right. A team led by Johan Commelin completed the Liquid Tensor Experiment in Lean in July 2022. Between these extremes lies a new mathematical practice: turning published mathematics into machine-checked proofs. It has its own methods (blueprints, libraries, collaboration at scale), its own failure modes (unfaithful statements, hidden axioms), and its own honest limits.

This lesson assumes that you have formalised some undergraduate mathematics in Lean (formalising mathematics in Lean and Mathlib), know the type theory underneath (type theory and propositions as types), and can reconstruct the omitted steps of a published proof (reading the mathematical literature). Formalisation is that last skill pushed to its limit.

IntuitionH

Three layers and a bridge

A formalisation has three layers, and it is useful to keep them apart.

The informal mathematics: the paper, with its definitions, lemmas and proofs, written for human readers who fill in routine steps.
The formal statements: definitions and theorem statements in the proof assistant's language. They are what the formalisation claims.
The formal proofs: terms that the checker's kernel verifies against the statements.

The kernel checks that layer 3 proves layer 2. Nothing checks automatically that layer 2 says what layer 1 says — that comparison is made by people. And layer 3 rarely mirrors layer 1 sentence by sentence: a formal proof fills every gap, often reorganises the argument, and usually replaces ad hoc constructions with general library results.

The bridge between the layers is a blueprint: a document that lists the definitions and lemmas, links each informal statement to its formal counterpart, and records which items each one uses. Because "uses" is a relation, a blueprint is a directed graph, and a project's progress can be read off it: what is stated, what is proved, what is ready to be attacked because everything it depends on is done.

Analogy, not a formal construction

A building's blueprint does not lay bricks, but it lets many builders work at once without colliding, and it shows the inspector what is supposed to be where. A mathematical blueprint does the same for a formalisation: it divides the work and makes the claims inspectable. The analogy stops at the inspection: a building inspector checks the bricks too, whereas a proof assistant checks every step mechanically and leaves people to inspect only the statements.

DefinitionsH

Definitions

Definition— blueprint

A blueprint for a formalisation project is a document that lists the definitions, lemmas and theorems to be formalised, gives for each an informal statement and proof and the name of its formal counterpart, and records the dependency relation: which earlier items each statement or proof uses. The dependency relation must be acyclic (a cycle would be a circular argument). An item is ready when everything it uses has been formalised.

Definition— faithful formal statement

A formal statement $\Phi$ is a faithful formalisation of an informal theorem $T$ if every reader who understands both agrees that $\Phi$ expresses $T$ : same hypotheses (none dropped, none added that are not in $T$ ), same conclusion, and definitions that agree with standard usage. A statement whose hypotheses are contradictory is vacuous: it is provable and says nothing.

Definition— trusted base

The trusted base of a formal proof is what must be trusted for the check to mean anything: the proof checker's kernel (and the hardware and software it runs on), the axioms the proof uses, and the formal statement together with every definition it mentions. Everything else — tactics, automation, the proof itself, however long — is checked and need not be trusted.

Definition— de Bruijn criterion

A proof assistant satisfies the de Bruijn criterion if every proof it accepts can be exported as an explicit proof object and re-checked by a small, independently written checker. This keeps the trusted kernel small and lets sceptics re-verify a formalisation without trusting the large system that produced it.

In Lean 4, the axioms behind a declaration are listed by #print axioms. Mathematical work in Mathlib uses three: propext (propositional extensionality), Quot.sound (quotients) and Classical.choice (the axiom of choice). Any further axiom — including sorryAx, which records an unfinished proof — is visible there.

Worked examplesH

A blueprint for Zagier's sentence

Here is the blueprint we used. Write $p = 4k + 1$ , and let $\zeta$ be Zagier's map and $\sigma(x, y, z) = (x, z, y)$ the swap. Items are definitions (def), lemmas (lem) and the theorem (thm); the last column lists what each item uses.

Item	Informal statement	Lean name	Uses
def:S	$S = \{(x, y, z) \in \N^3 : x^2 + 4yz = p\}$	`zagierSet`	—
def:map	Zagier's piecewise map $\zeta$	`zagierMap`	—
def:swap	$\sigma(x, y, z) = (x, z, y)$	`swapMap`	—
lem:facts	on $S$ : $x, y, z > 0$ , $x \ne y - z$ , $x \ne 2y$	`zagier_facts`	def:S
lem:finite	$S$ is finite (all coordinates at most $p$ )	`mem_zagierSet`	def:S, lem:facts
lem:cases	each case of $\zeta$ preserves $x^2 + 4yz$	`zagierMap_eq_one`, …	def:map
lem:mapsto	$\zeta$ maps $S$ to $S$	`zagierMap_mapsTo`	lem:cases, lem:finite
lem:invol	$\zeta(\zeta(t)) = t$ on $S$	`zagierMap_involutive`	def:map, lem:facts, lem:finite
lem:fixed	the only fixed point of $\zeta$ on $S$ is $(1, 1, k)$	`zagier_fixed_points`	def:map, lem:facts, lem:finite
lem:parity	an involution of a finite set has as many fixed points as elements, mod 2	`card_mod_two_of_involution`	—
lem:odd	$S$ has an odd number of elements	`card_zagierSet_odd`	lem:mapsto, lem:invol, lem:fixed, lem:parity
thm:fermat	$p$ is a sum of two squares	`zagier_two_squares`	def:swap, lem:odd, lem:parity, lem:finite

The dependency graph, drawn without the arrows that follow from others by transitivity (an arrow $A \to B$ means " $B$ uses $A$ "):

The blueprint's dependency graph (transitive reduction). The parity lemma and the swap are independent of the rest; the chain def:S → lem:facts → lem:finite → lem:mapsto → lem:odd → thm:fermat is a longest path.

Example— What the sentence leaves unsaid

Formalising the blueprint brought the following to the surface. None of them is an error — Zagier's proof is correct — but each is a step a proof checker needs and a reader supplies silently.

"The finite set." If $\N$ contains $0$ (as in Lean), $S$ is finite only because $p$ is not a perfect square: for $n = 9$ the triples $(3, 0, z)$ lie in $S$ for every $z$ . For prime $p$ , $y = 0$ or $z = 0$ would give $x^2 = p$ ; so all coordinates are positive and bounded by $p$ . Lean needs an explicit bound to make $S$ a finite set.
Positivity. $x > 0$ because $p$ is odd; $y, z > 0$ because $p$ is not a square. The case analysis silently uses all three.
The boundaries. The three cases cover $x < y - z$ , $y - z < x < 2y$ and $x > 2y$ , but not $x = y - z$ or $x = 2y$ . These never occur on $S$ : $x = y - z$ gives $p = (x + 2z)^2$ , a square, and $x = 2y$ gives $p = 4y(y + z)$ , which is even.
Transcription. In $\N$ , Lean's subtraction is truncated ( $2 - 5 = 0$ ). The formula $x - y + z$ must be written $x + z - y$ , and the condition $x < y - z$ as $x + z < y$ ; on $S$ these agree with the paper.
"Involution", "exactly one fixed point". Both are case analyses that the paper leaves to the reader: case 1 is sent to case 3 and back, case 2 to itself; fixed points force $x = y$ , and then $x(x + 4z) = p$ forces $x = 1$ because $p$ is prime.
"So $|S|$ is odd." This uses a lemma the sentence does not state: an involution of a finite set has as many fixed points as elements, modulo $2$ .
The last step. A fixed point of the swap is $(x, y, y)$ , and then $p = x^2 + 4y^2 = x^2 + (2y)^2$ — the conclusion the sentence leaves to the reader.
The statement. The formalised theorem is stated for $p = 4k + 1$ ; a separate one-line lemma converts it to " $p$ prime and $p \equiv 1 \pmod 4$ ".

Primality is used in exactly two places — to exclude squares (items 1–3) and to force $x = 1$ (item 5) — and oddness once. For $n = 21 = 3 \cdot 7$ the map has two fixed points, $(1, 1, 5)$ and $(3, 3, 1)$ , the parity argument collapses, and indeed $21$ is not a sum of two squares.

A windmill for $(x, y, z) = (3, 1, 5)$: a central $3 \times 3$ square and four $1 \times 5$ arms, of total area $3^2 + 4 \cdot 1 \cdot 5 = 29$. Every element of $S$ is such a windmill of area $p$. The swap $(x, y, z) \mapsto (x, z, y)$ is a reflection; its fixed points are windmills with square arms, and four $y \times y$ squares make one $2y \times 2y$ square — hence $p = x^2 + (2y)^2$.

ProofH

The proof, with nothing left out

Here is Zagier's argument written out in full, item by item, so that it can be compared line by line with the Lean code below. Throughout, $p = 4k + 1$ is prime and $S = \{(x, y, z) \in \N^3 : x^2 + 4yz = p\}$ , with $0 \in \N$ .

Theorem— Lemma 1 (facts about S)

If $(x, y, z) \in S$ , then $x, y, z \ge 1$ , $x + z \ne y$ and $x \ne 2y$ . Consequently $x, y, z \le p$ , and $S$ is finite.

Proof

A prime is not a perfect square: if $m^2 = p$ then $m \mid p$ , so $m \in \{1, p\}$ , and neither $1^2$ nor $p^2$ equals $p$ . If $x = 0$ then $p = 4yz \equiv 0 \pmod 4$ , which is false. If $y = 0$ or $z = 0$ then $p = x^2$ , a square. If $y = x + z$ then $p = x^2 + 4(x + z)z = (x + 2z)^2$ . If $x = 2y$ then $p = 4y^2 + 4yz \equiv 0 \pmod 4$ . Finally $x \le x^2 \le p$ , and $y \le 4yz \le p$ because $z \ge 1$ ; similarly $z \le p$ .

∎

Theorem— Lemma 2 (the map preserves S)

Let $\zeta$ be Zagier's map, with the three cases as in the paper. For $t \in S$ , $\zeta(t) \in S$ .

Proof

By Lemma 1, every $t = (x, y, z) \in S$ falls in exactly one case, and the new coordinates are natural numbers. In case 1 ( $x + z < y$ ): $(x + 2z)^2 + 4z(y - x - z) = x^2 + 4xz + 4z^2 + 4yz - 4xz - 4z^2 = x^2 + 4yz$ . In case 2: $(2y - x)^2 + 4y(x + z - y) = 4y^2 - 4xy + x^2 + 4xy + 4yz - 4y^2 = x^2 + 4yz$ . In case 3 ( $x > 2y$ ): $(x - 2y)^2 + 4(x + z - y)y = x^2 - 4xy + 4y^2 + 4xy + 4yz - 4y^2 = x^2 + 4yz$ .

∎

Theorem— Lemma 3 (involution)

$\zeta(\zeta(t)) = t$ for every $t \in S$ .

Proof

Let $t = (x, y, z)$ ; by Lemma 1, $x, y, z \ge 1$ and $t$ is not on a boundary. In case 1, $\zeta(t) = (x + 2z, z, y - x - z)$ , and its first coordinate exceeds twice its second ( $x + 2z > 2z$ since $x \ge 1$ ), so case 3 applies: $\zeta(\zeta(t)) = (x + 2z - 2z,\; (x + 2z) - z + (y - x - z),\; z) = (x, y, z)$ . In case 3, $\zeta(t) = (x - 2y, x - y + z, y)$ , and $(x - 2y) + y < x - y + z$ since $z \ge 1$ , so case 1 applies and returns $(x, y, z)$ . In case 2, $\zeta(t) = (2y - x, y, x - y + z)$ with $y - (x - y + z) = 2y - x - z < 2y - x$ (as $z \ge 1$ ) and $2y - x < 2y$ (as $x \ge 1$ ), so case 2 applies again and returns $(2y - (2y - x),\; y,\; (2y - x) - y + (x - y + z)) = (x, y, z)$ .

∎

Theorem— Lemma 4 (exactly one fixed point)

The only fixed point of $\zeta$ on $S$ is $(1, 1, k)$ .

Proof

A fixed point in case 1 would have $x + 2z = x$ , so $z = 0$ ; in case 3, $x - 2y = x$ , so $y = 0$ ; both contradict Lemma 1. In case 2, $\zeta(t) = t$ means $2y - x = x$ , that is $x = y$ . Then $p = x^2 + 4xz = x(x + 4z)$ , so $x \mid p$ ; since $x + 4z \ge 5 > 1$ , $x \ne p$ , hence $x = 1 = y$ and $1 + 4z = 4k + 1$ , so $z = k$ . Conversely $(1, 1, k) \in S$ is in case 2 and is fixed.

∎

Theorem— Lemma 5 (parity)

If $f$ is an involution of a finite set $A$ (that is, $f(A) \subseteq A$ and $f(f(a)) = a$ for $a \in A$ ), then $|A| \equiv |\{a \in A : f(a) = a\}| \pmod 2$ .

Proof

Strong induction on $|A|$ . If $A = \varnothing$ both sides are $0$ . Otherwise pick $a \in A$ . If $f(a) = a$ , then $f$ restricts to an involution of $A \setminus \{a\}$ (if $f(b) = a$ for $b \ne a$ then $b = f(f(b)) = f(a) = a$ ), which has one element and one fixed point fewer. If $f(a) \ne a$ , then $f$ restricts to an involution of $A \setminus \{a, f(a)\}$ , which has two elements fewer and the same fixed points (neither $a$ nor $f(a)$ is fixed, as $f(f(a)) = a \ne f(a)$ ). In both cases the induction hypothesis gives the claim.

∎

Theorem— Theorem (Fermat; Zagier's proof)

Every prime $p \equiv 1 \pmod 4$ is a sum of two squares.

Proof

Write $p = 4k + 1$ . By Lemmas 2–5, $|S| \equiv 1 \pmod 2$ . The swap $\sigma(x, y, z) = (x, z, y)$ maps $S$ to $S$ and is an involution, so by Lemma 5 it has an odd number of fixed points — in particular one, $(x, y, y) \in S$ . Then $p = x^2 + 4y^2 = x^2 + (2y)^2$ .

∎

The argument has a classical pedigree: the theorem was stated by Fermat in a letter of 1640 without proof and proved by Euler in the 1740s and 1750s; Zagier's sentence condenses a proof by Roger Heath-Brown (1984), which was in turn inspired by work of Liouville.

ExplanationH

Large formalisations: what they did and did not verify

Zagier's proof takes an afternoon to formalise. The projects below took years, and each taught the community something.

The four colour theorem (Georges Gonthier, with Benjamin Werner, Coq, completed 2005). Appel and Haken's 1976 proof, and the 1997 proof of Robertson, Sanders, Seymour and Thomas, rely on computer checks of many hundreds of configurations. Gonthier formalised the whole argument, including the computations, so that the computer-assisted part is checked by the same kernel as the rest. Formalising the statement required a precise combinatorial notion of planar map (hypermaps), because the topological statement about the plane had to be connected to a finite one.
The odd order theorem (Gonthier and a team of about fifteen, Coq with the Mathematical Components library, completed September 2012). Feit and Thompson's 1963 proof filled a 255-page issue of the Pacific Journal of Mathematics. The formalisation did not follow that paper line by line: it followed the later, reorganised accounts of Bender and Glauberman (1994) and Peterfalvi (2000), and along the way it built libraries of finite group theory, linear algebra and character theory that were then reused.
The Kepler conjecture (Thomas Hales and collaborators, the Flyspeck project in HOL Light and Isabelle, completed 2014, published 2017). Hales's proof (with Samuel Ferguson), announced in 1998 and published in the Annals of Mathematics in 2005, combined geometry with extensive computer calculations; the referees reported that they could not certify every part. Flyspeck formally verified the geometry, the enumeration of "tame" graphs, the linear programs, and the nonlinear inequalities proved by interval arithmetic.
The Liquid Tensor Experiment (Johan Commelin, Adam Topaz and many others, Lean 3 with mathlib, December 2020 to July 2022). It verified Clausen and Scholze's main theorem on liquid real vector spaces, a statement about Ext groups of condensed abelian groups. The team organised the work around a blueprint, formalised the key technical theorem first (by June 2021), and had to develop a substantial amount of condensed mathematics and homological algebra in Lean along the way. Scholze wrote that the process improved his own understanding of the proof.
Recent and ongoing. The sphere eversion project (Floris van Doorn, Patrick Massot and Oliver Nash, presented in 2023) formalised Gromov's h-principle for open ample relations and deduced Smale's sphere eversion; Massot's blueprint software grew out of it. In November 2023, Gowers, Green, Manners and Tao posted a proof of Marton's conjecture (the polynomial Freiman–Ruzsa conjecture), and a collaborative Lean project coordinated by Tao formalised it within about three weeks. Kevin Buzzard's project to formalise a proof of Fermat's Last Theorem in Lean began in 2024 and is ongoing.

What these projects verified. In each case: that the formal statement follows from the axioms of the system, as checked by its kernel. What they did not verify: that the formal statement is the theorem mathematicians care about (people checked this, by reading the statements and the definitions they rest on); that the original paper's proof is correct as written (the formal proof may follow a different route, as with the odd order theorem); that the result is important; or anything about results the project did not formalise. Formalisation lowers the chance of error in what it covers almost to zero; it does not replace reading, refereeing and judgement.

Working on a library. Contributing a formalisation to Mathlib adds constraints that a one-off project does not have: state results at their natural generality (for rings, not just $\Z$ ; for topological spaces, not just $\R$ ); reuse existing definitions rather than duplicating them; follow the naming and documentation conventions; and accept review. Mathlib's contributors review every change, and the library is continually refactored as better abstractions appear. A good first contribution fills a small, well-defined gap that a project of your own needed.

Formal mathematicsF

Zagier's proof in Lean

The module formalises the blueprint completely, in Lean 4 with Mathlib. Each blueprint item corresponds to one or a few declarations, and the proofs mirror the human proofs above.

The set and the facts the sentence uses silently. We define $S$ as a finite set by filtering a box, and then show that for prime $p$ the box cuts nothing off.

zagierSetLean 4Formally verified

/-- Zagier's set `S = {(x, y, z) ∈ ℕ³ : x² + 4yz = p}` for `p = 4k + 1`. The paper calls `S` "the
finite set" without comment; to make finiteness explicit we define `S` as a `Finset`, filtering
the box `{0, …, p}³`, and prove in `mem_zagierSet` that the box cuts nothing off. -/
def zagierSet (k : ℕ) : Finset (ℕ × ℕ × ℕ) :=
  ((range (4 * k + 2)) ×ˢ (range (4 * k + 2)) ×ˢ (range (4 * k + 2))).filter
    (fun t => t.1 ^ 2 + 4 * t.2.1 * t.2.2 = 4 * k + 1)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagier_factsLean 4Proved here from basic factsFormally verified

/-- The facts that Zagier's sentence uses without stating them. If `p = 4k + 1` is prime and
`x² + 4yz = p`, then `x, y, z > 0`, and neither boundary case occurs: `x + z ≠ y` (otherwise
`p = (x + 2z)²` would be a square) and `x ≠ 2y` (otherwise `p = 4y(y + z)` would be even). -/
theorem zagier_facts {k x y z : ℕ} (hp : (4 * k + 1).Prime) (h : x ^ 2 + 4 * y * z = 4 * k + 1) :
    0 < x ∧ 0 < y ∧ 0 < z ∧ x + z ≠ y ∧ x ≠ 2 * y := by
  -- A prime is never a perfect square.
  have not_square : ∀ m : ℕ, m * m ≠ 4 * k + 1 := by
    intro m hm
    rw [← hm] at hp
    rcases Nat.prime_mul_iff.1 hp with ⟨hm1, rfl⟩ | ⟨hm1, rfl⟩ <;> exact Nat.not_prime_one hm1
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · -- `x = 0` would make `p = 4yz` divisible by 4.
    rcases Nat.eq_zero_or_pos x with rfl | hx
    · have : 4 * (y * z) = 4 * k + 1 := by rw [← h]; ring
      omega
    · exact hx
  · rcases Nat.eq_zero_or_pos y with rfl | hy
    · exact absurd (by rw [← h]; ring) (not_square x)
    · exact hy
  · rcases Nat.eq_zero_or_pos z with rfl | hz
    · exact absurd (by rw [← h]; ring) (not_square x)
    · exact hz
  · intro hb
    subst hb
    exact not_square (x + 2 * z) (by rw [← h]; ring)
  · intro hb
    subst hb
    have : 4 * (y * y + y * z) = 4 * k + 1 := by rw [← h]; ring
    omega

Axioms used: propext, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

mem_zagierSetLean 4Proved here from basic factsFormally verified

/-- For prime `p = 4k + 1`, a triple lies in `zagierSet k` exactly when `x² + 4yz = p`: every
solution already lies in the box `{0, …, p}³`, because `x ≤ x²`, `y ≤ 4yz` and `z ≤ 4yz`. -/
theorem mem_zagierSet {k : ℕ} (hp : (4 * k + 1).Prime) {t : ℕ × ℕ × ℕ} :
    t ∈ zagierSet k ↔ t.1 ^ 2 + 4 * t.2.1 * t.2.2 = 4 * k + 1 := by
  obtain ⟨x, y, z⟩ := t
  simp only [zagierSet, mem_filter, mem_product, mem_range, and_iff_right_iff_imp]
  intro h
  obtain ⟨hx, hy, hz, -, -⟩ := zagier_facts hp h
  refine ⟨?_, ?_, ?_⟩ <;> nlinarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

The map. The definition follows the paper's case order, with truncated subtraction handled as in item 4 of the list of gaps. Two of the three case lemmas:

zagierMapLean 4Formally verified

/-- Zagier's piecewise map, transcribed with the conditions in the paper's order. In `ℕ`,
subtraction is truncated (`2 - 5 = 0`), so the condition `x < y − z` is written `x + z < y`, and
`x − y + z` is written `x + z − y`; on `S` these agree with the integer formulas. -/
def zagierMap : ℕ × ℕ × ℕ → ℕ × ℕ × ℕ
  | (x, y, z) =>
    if x + z < y then (x + 2 * z, z, y - x - z)
    else if x < 2 * y then (2 * y - x, y, x + z - y)
    else (x - 2 * y, x + z - y, y)

Axioms used: No axiomsformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagierMap_eq_oneLean 4Proved here from basic factsFormally verified

/-- Case 1 preserves `x² + 4yz`: if `x + z < y` then
`(x + 2z)² + 4z(y − x − z) = x² + 4yz`. -/
theorem zagierMap_eq_one {x y z : ℕ} (h : x + z < y) :
    (x + 2 * z) ^ 2 + 4 * z * (y - x - z) = x ^ 2 + 4 * y * z := by
  obtain ⟨d, rfl⟩ : ∃ d, y = x + z + d := ⟨y - (x + z), by omega⟩
  rw [show x + z + d - x - z = d by omega]
  ring

Axioms used: propext, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagierMap_eq_twoLean 4Proved here from basic factsFormally verified

/-- Case 2 preserves `x² + 4yz`: if `y ≤ x + z` and `x ≤ 2y` then
`(2y − x)² + 4y(x + z − y) = x² + 4yz`. Proved by passing to `ℤ`, where subtraction is honest. -/
theorem zagierMap_eq_two {x y z : ℕ} (h₁ : y ≤ x + z) (h₂ : x ≤ 2 * y) :
    (2 * y - x) ^ 2 + 4 * y * (x + z - y) = x ^ 2 + 4 * y * z := by
  zify [h₁, h₂]
  ring

Axioms used: propext, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagierMap_mapsToLean 4Proved here from basic factsFormally verified

/-- Zagier's map sends `S` into `S` (the word "on" in "the involution on the finite set `S`"). -/
theorem zagierMap_mapsTo {k : ℕ} (hp : (4 * k + 1).Prime) {t : ℕ × ℕ × ℕ}
    (ht : t ∈ zagierSet k) : zagierMap t ∈ zagierSet k := by
  obtain ⟨x, y, z⟩ := t
  rw [mem_zagierSet hp] at ht ⊢
  simp only at ht
  simp only [zagierMap]
  split_ifs with h₁ h₂
  · rw [← ht]; exact zagierMap_eq_one h₁
  · rw [← ht]; exact zagierMap_eq_two (by omega) h₂.le
  · rw [← ht]; exact zagierMap_eq_three (by omega)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagierMap_involutiveLean 4Proved here from basic factsFormally verified

/-- Zagier's map is an involution on `S` ("easily checked" in the paper). Case 1 is sent to
case 3 and back, case 2 to itself. The proof uses `x, y, z > 0` and the absence of boundary
cases from `zagier_facts`; without them the map is not an involution. -/
theorem zagierMap_involutive {k : ℕ} (hp : (4 * k + 1).Prime) {t : ℕ × ℕ × ℕ}
    (ht : t ∈ zagierSet k) : zagierMap (zagierMap t) = t := by
  obtain ⟨x, y, z⟩ := t
  rw [mem_zagierSet hp] at ht
  simp only at ht
  obtain ⟨hx, hy, hz, hb₁, hb₂⟩ := zagier_facts hp ht
  by_cases h₁ : x + z < y
  · -- Case 1 lands in case 3.
    have e : zagierMap (x, y, z) = (x + 2 * z, z, y - x - z) := by simp [zagierMap, h₁]
    rw [e]
    simp only [zagierMap]
    rw [ite_eq_right (by omega), ite_eq_right (by omega)]
    refine Prod.ext ?_ (Prod.ext ?_ ?_) <;> dsimp only <;> omega
  · by_cases h₂ : x < 2 * y
    · -- Case 2 lands in case 2.
      have e : zagierMap (x, y, z) = (2 * y - x, y, x + z - y) := by simp [zagierMap, h₁, h₂]
      rw [e]
      simp only [zagierMap]
      rw [ite_eq_right (by omega), ite_eq_left (by omega)]
      refine Prod.ext ?_ (Prod.ext ?_ ?_) <;> dsimp only <;> omega
    · -- Case 3 lands in case 1.
      have e : zagierMap (x, y, z) = (x - 2 * y, x + z - y, y) := by simp [zagierMap, h₁, h₂]
      rw [e]
      simp only [zagierMap]
      rw [ite_eq_left (by omega)]
      refine Prod.ext ?_ (Prod.ext ?_ ?_) <;> dsimp only <;> omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

Exactly one fixed point, then the parity lemma, proved here by induction exactly as in Lemma 5:

zagierMap_fixed_iffLean 4Proved here from basic factsFormally verified

/-- On `S`, a triple is fixed by Zagier's map exactly when `x = y`. (Cases 1 and 3 have no
fixed points because they would force `z = 0` or `y = 0`.) -/
theorem zagierMap_fixed_iff {k x y z : ℕ} (hp : (4 * k + 1).Prime)
    (ht : x ^ 2 + 4 * y * z = 4 * k + 1) : zagierMap (x, y, z) = (x, y, z) ↔ x = y := by
  obtain ⟨hx, hy, hz, hb₁, hb₂⟩ := zagier_facts hp ht
  simp only [zagierMap]
  split_ifs with h₁ h₂ <;> rw [Prod.ext_iff, Prod.ext_iff] <;> dsimp only <;> omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagier_fixed_pointsLean 4Proved here from basic factsFormally verified

/-- The unique fixed point. If `x = y` then `x(x + 4z) = p`; as `p` is prime and `x + 4z > 1`,
`x = 1`, and then `z = k`. So the fixed points of Zagier's map on `S` are exactly `{(1, 1, k)}`. -/
theorem zagier_fixed_points {k : ℕ} (hp : (4 * k + 1).Prime) :
    (zagierSet k).filter (fun t => zagierMap t = t) = {(1, 1, k)} := by
  ext ⟨x, y, z⟩
  simp only [mem_filter, mem_singleton, Prod.mk.injEq]
  constructor
  · rintro ⟨ht, hfix⟩
    rw [mem_zagierSet hp] at ht
    simp only at ht
    have hxy : x = y := (zagierMap_fixed_iff hp ht).1 hfix
    subst hxy
    obtain ⟨hx, -, hz, -, -⟩ := zagier_facts hp ht
    -- `x` divides `p = x * (x + 4z)`, so `x = 1` or `x = p`.
    have hdvd : x ∣ 4 * k + 1 := ⟨x + 4 * z, by rw [← ht]; ring⟩
    rcases hp.eq_one_or_self_of_dvd x hdvd with rfl | hxp
    · refine ⟨rfl, rfl, ?_⟩
      norm_num at ht
      omega
    · -- `x = p` is impossible: then `p² ≤ x² + 4xz = p`.
      exfalso
      have : (4 * k + 1) * (4 * k + 1) ≤ 4 * k + 1 := by
        calc (4 * k + 1) * (4 * k + 1) = x ^ 2 := by rw [hxp]; ring
          _ ≤ x ^ 2 + 4 * x * z := Nat.le_add_right _ _
          _ = 4 * k + 1 := ht
      nlinarith
  · rintro ⟨rfl, rfl, rfl⟩
    refine ⟨(mem_zagierSet hp).2 (by ring), ?_⟩
    rw [zagierMap_fixed_iff hp (by ring)]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

card_mod_two_of_involutionLean 4Proved here from basic factsFormally verified

/-- **Parity lemma.** If `f` is an involution of a finite set `s`, then `s` and the set of fixed
points of `f` have the same parity. Proof by strong induction: remove a fixed point, or remove a
two-element orbit `{x, f x}`. (Mathlib has a more general version for any prime `p`:
`Equiv.Perm.card_fixedPoints_modEq`.) -/
theorem card_mod_two_of_involution {α : Type*} [DecidableEq α] (f : α → α) (s : Finset α)
    (hmaps : ∀ x ∈ s, f x ∈ s) (hinv : ∀ x ∈ s, f (f x) = x) :
    s.card % 2 = (s.filter (fun x => f x = x)).card % 2 := by
  induction s using Finset.strongInduction with
  | H s ih =>
    rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
    · simp
    by_cases hfx : f x = x
    · -- Remove the fixed point `x`.
      have hmaps' : ∀ y ∈ s.erase x, f y ∈ s.erase x := by
        intro y hy
        rw [mem_erase] at hy ⊢
        refine ⟨fun hfy => hy.1 ?_, hmaps y hy.2⟩
        calc y = f (f y) := (hinv y hy.2).symm
          _ = x := by rw [hfy, hfx]
      have IH := ih (s.erase x) (erase_ssubset hx) hmaps'
        (fun y hy => hinv y (mem_of_mem_erase hy))
      have hfilter : (s.erase x).filter (fun y => f y = y) =
          (s.filter (fun y => f y = y)).erase x := by
        ext y
        simp only [mem_filter, mem_erase]
        tauto
      have h₁ := card_erase_add_one hx
      have hxF : x ∈ s.filter (fun y => f y = y) := mem_filter.2 ⟨hx, hfx⟩
      have h₂ := card_erase_add_one hxF
      rw [hfilter] at IH
      omega
    · -- Remove the two-element orbit `{x, f x}`.
      have hfxs : f x ∈ s.erase x := mem_erase.2 ⟨hfx, hmaps x hx⟩
      have hmaps' : ∀ y ∈ (s.erase x).erase (f x), f y ∈ (s.erase x).erase (f x) := by
        intro y hy
        simp only [mem_erase] at hy ⊢
        obtain ⟨hy₁, hy₂, hy₃⟩ := hy
        refine ⟨fun h => hy₂ ?_, fun h => hy₁ ?_, hmaps y hy₃⟩
        · calc y = f (f y) := (hinv y hy₃).symm
            _ = x := by rw [h, hinv x hx]
        · calc y = f (f y) := (hinv y hy₃).symm
            _ = f x := by rw [h]
      have IH := ih ((s.erase x).erase (f x))
        ((erase_ssubset hfxs).trans (erase_ssubset hx)) hmaps'
        (fun y hy => hinv y (mem_of_mem_erase (mem_of_mem_erase hy)))
      have hfilter : ((s.erase x).erase (f x)).filter (fun y => f y = y) =
          s.filter (fun y => f y = y) := by
        ext y
        simp only [mem_filter, mem_erase]
        constructor
        · rintro ⟨⟨-, -, hy⟩, hfy⟩
          exact ⟨hy, hfy⟩
        · rintro ⟨hy, hfy⟩
          refine ⟨⟨fun h => ?_, fun h => hfx (h ▸ hfy), hy⟩, hfy⟩
          -- `f x` is not fixed, since `f (f x) = x ≠ f x`.
          rw [h, hinv x hx] at hfy
          exact hfx hfy.symm
      have h₁ := card_erase_add_one hx
      have h₂ := card_erase_add_one hfxs
      rw [hfilter] at IH
      omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

card_zagierSet_oddLean 4Proved here from basic factsFormally verified

/-- "So `|S|` is odd": Zagier's map is an involution of `S` with exactly one fixed point. -/
theorem card_zagierSet_odd {k : ℕ} (hp : (4 * k + 1).Prime) : (zagierSet k).card % 2 = 1 := by
  rw [card_mod_two_of_involution zagierMap (zagierSet k)
    (fun t ht => zagierMap_mapsTo hp ht) (fun t ht => zagierMap_involutive hp ht),
    zagier_fixed_points hp, card_singleton]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

The theorem.

swapMapLean 4Formally verified

/-- The "obvious" involution `(x, y, z) ↦ (x, z, y)` of `S`. -/
def swapMap : ℕ × ℕ × ℕ → ℕ × ℕ × ℕ
  | (x, y, z) => (x, z, y)

Axioms used: No axiomsformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

zagier_two_squaresLean 4Proved here from basic factsFormally verified

/-- **Fermat's two-squares theorem, by Zagier's argument.** If `p = 4k + 1` is prime then `p` is
a sum of two squares. The swap is an involution of `S`; since `|S|` is odd it has an odd number of
fixed points, hence at least one, `(x, y, y)`, and then `p = x² + 4y² = x² + (2y)²`. -/
theorem zagier_two_squares (k : ℕ) (hp : (4 * k + 1).Prime) :
    ∃ a b : ℕ, a ^ 2 + b ^ 2 = 4 * k + 1 := by
  have hmaps : ∀ t ∈ zagierSet k, swapMap t ∈ zagierSet k := by
    rintro ⟨x, y, z⟩ ht
    rw [mem_zagierSet hp] at ht ⊢
    simp only [swapMap] at ht ⊢
    rw [← ht]; ring
  have hinv : ∀ t ∈ zagierSet k, swapMap (swapMap t) = t := by
    rintro ⟨x, y, z⟩ -
    rfl
  have hpar := card_mod_two_of_involution swapMap (zagierSet k) hmaps hinv
  rw [card_zagierSet_odd hp] at hpar
  -- An odd number is not zero, so the swap has a fixed point.
  obtain ⟨⟨x, y, z⟩, ht⟩ : ((zagierSet k).filter (fun t => swapMap t = t)).Nonempty := by
    rw [← card_pos]
    omega
  rw [mem_filter, mem_zagierSet hp] at ht
  obtain ⟨ht, hfix⟩ := ht
  simp only [swapMap, Prod.mk.injEq] at hfix ht
  obtain ⟨-, hzy, -⟩ := hfix
  subst hzy
  exact ⟨x, 2 * z, by rw [← ht]; ring⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

Checking the statement. The formal theorem is stated for $p = 4k + 1$ . To check faithfulness we derive the usual form, and compare it with Mathlib's theorem, whose proof is entirely different (it uses unique factorisation in the Gaussian integers $\Z[i]$ ) and whose hypothesis $p \% 4 \ne 3$ also covers $p = 2$ . That two independent formal proofs reach statements we can compare by eye is itself a check on layer 2.

prime_one_mod_fourLean 4Proved here from basic factsFormally verified

/-- The published statement, in its usual form: every prime `p ≡ 1 (mod 4)` is a sum of two
squares. Deduced from `zagier_two_squares` with `k = p / 4`; this small step is the check that
"`p = 4k + 1`" and "`p ≡ 1 (mod 4)`" say the same thing. -/
theorem prime_one_mod_four {p : ℕ} (hp : p.Prime) (h4 : p % 4 = 1) :
    ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by
  have hk : 4 * (p / 4) + 1 = p := by omega
  rw [← hk] at hp ⊢
  exact zagier_two_squares (p / 4) hp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

two_squares_libraryLean 4Applies a library theoremFormally verified

/-- The same theorem from Mathlib: `Nat.Prime.sq_add_sq` proves that every prime `p` with
`p % 4 ≠ 3` is a sum of two squares (so it also covers `p = 2 = 1² + 1²`), by a different
proof through the unique factorisation of the Gaussian integers `ℤ[i]`. -/
theorem two_squares_library {p : ℕ} (hp : p.Prime) (h4 : p % 4 = 1) :
    ∃ a b : ℕ, a ^ 2 + b ^ 2 = p :=
  haveI := Fact.mk hp
  Nat.Prime.sq_add_sq (by omega)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

A hypothesis cannot be dropped. The formal counterpart of the remark about $21$ :

primality_neededLean 4Proved here from basic factsFormally verified

/-- Where the hypothesis "prime" is used. For `21 = 4·5 + 1`, which is not prime, Zagier's map
has *two* fixed points in `S`, `(1, 1, 5)` and `(3, 3, 1)`, so the parity argument collapses — and
indeed `21` is not a sum of two squares. -/
theorem primality_needed :
    (1 ^ 2 + 4 * 1 * 5 = 21 ∧ zagierMap (1, 1, 5) = (1, 1, 5)) ∧
    (3 ^ 2 + 4 * 3 * 1 = 21 ∧ zagierMap (3, 3, 1) = (3, 3, 1)) ∧
    ¬ ∃ a b : ℕ, a ^ 2 + b ^ 2 = 21 := by
  refine ⟨by decide, by decide, ?_⟩
  rintro ⟨a, b, h⟩
  have ha : a < 5 := by nlinarith
  have hb : b < 5 := by nlinarith
  interval_cases a <;> interval_cases b <;> omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FormalisingPublishedMathematics.leanTry it in the Lean web editor

What is and is not formalised. Everything in Zagier's sentence is formalised, with every gap filled; #print axioms on zagier_two_squares reports only Lean's standard axioms (propext, Classical.choice, Quot.sound). The trusted base is therefore Lean's kernel, those axioms, and the statements above — in particular Mathlib's definition of Nat.Prime, which you can read. Not formalised here: the windmill picture, and the history. Mathlib's Archive/ZagierTwoSquares.lean (Jeremy Tan and Thomas Browning, 2023) contains another formalisation of the same proof, written differently; comparing two independent formalisations of one argument is instructive.

ComputationC

Testing before proving, and managing the blueprint

Before formalising, test every claim of the proof on many cases — it is cheap, and a failed test points straight at a missing hypothesis. The first experiment checks each assertion of Zagier's sentence for all primes $p \equiv 1 \pmod 4$ below $3000$ , and then for composite $n \equiv 1 \pmod 4$ , where it shows exactly which assertion fails.

Zagier's involution, tested claim by claimPythonExact computationExhaustive finite checkComputationally tested

"""Stress-testing a published proof before (and after) formalising it.

Don Zagier's one-sentence proof (1990) that every prime p = 1 (mod 4) is a
sum of two squares uses an involution of the finite set
S = {(x, y, z) : x^2 + 4yz = p} with exactly one fixed point. Before
formalising such a proof it pays to test every claim it makes on many cases,
and to see which hypothesis each claim needs.

For every prime p = 1 (mod 4) below a bound we compute S, apply Zagier's map,
and check: no triple lies on a boundary between the three cases, the map sends
S into S and is an involution, it has exactly one fixed point (1, 1, k), |S|
is odd, and the swap (x, y, z) -> (x, z, y) has a fixed point giving
p = x^2 + (2y)^2. Then we run the same checks on numbers n = 1 (mod 4) that
are not prime, to see exactly where the argument breaks. Triples are taken
with positive coordinates; with 0 allowed, S is infinite when n is a square.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from math import isqrt
import textwrap

def is_prime(n):
    """Trial-division primality test."""
    return n >= 2 and all(n % d for d in range(2, isqrt(n) + 1))

def zagier_set(n):
    """All (x, y, z) with x, y, z >= 1 and x^2 + 4yz = n, sorted."""
    triples = []
    for x in range(1, isqrt(n) + 1):
        rest = n - x * x
        if rest <= 0 or rest % 4:
            continue
        m = rest // 4
        triples.extend((x, y, m // y) for y in range(1, m + 1) if m % y == 0)
    return sorted(triples)

def on_boundary(t):
    """Is t on a boundary between Zagier's cases (x = y - z or x = 2y)?"""
    x, y, z = t
    return x == y - z or x == 2 * y

def zagier_map(t):
    """Zagier's piecewise map, with the paper's three cases."""
    x, y, z = t
    if x < y - z:
        return (x + 2 * z, z, y - x - z)
    if x < 2 * y:
        return (2 * y - x, y, x - y + z)
    return (x - 2 * y, x - y + z, y)

def swap(t):
    """The obvious involution (x, y, z) -> (x, z, y)."""
    x, y, z = t
    return (x, z, y)

def audit(n):
    """Check each claim of the proof for n; return a dict of findings."""
    s = zagier_set(n)
    members = set(s)
    images = [zagier_map(t) for t in s]
    fixed = [t for t, u in zip(s, images) if u == t]
    swap_fixed = [t for t in s if swap(t) == t]
    return {
        "size": len(s),
        "boundary": [t for t in s if on_boundary(t)],
        "maps_into": all(u in members for u in images),
        "involution": all(zagier_map(u) == t for t, u in zip(s, images)),
        "fixed": fixed,
        "swap_fixed": swap_fixed,
        "squares": [(x, 2 * y) for x, y, _ in swap_fixed],
    }

def claims_hold(n, report):
    """Do all claims of Zagier's sentence hold for n = 4k + 1?"""
    k = (n - 1) // 4
    return (not report["boundary"] and report["maps_into"]
            and report["involution"] and report["fixed"] == [(1, 1, k)]
            and report["size"] % 2 == 1 and len(report["swap_fixed"]) >= 1)

def main():
    bound = 3000
    primes = [p for p in range(5, bound, 4) if is_prime(p)]
    good = [p for p in primes if claims_hold(p, audit(p))]
    sizes = [audit(p)["size"] for p in primes]
    print(f"Primes p = 1 (mod 4) below {bound}: {len(primes)}")
    print(f"All claims of the sentence hold for {len(good)} of them")
    print(f"|S| ranges from {min(sizes)} to {max(sizes)}; always odd: "
          f"{all(m % 2 for m in sizes)}")
    for p in primes[:3] + [primes[-1]]:
        r = audit(p)
        a, b = r["squares"][0]
        print(f"   p = {p:>4}: |S| = {r['size']:>3}, fixed point {r['fixed'][0]},"
              f" p = {a}^2 + {b}^2")
    print()
    print("Composite n = 1 (mod 4): which claims fail?")
    print("   (fixed = fixed points of Zagier's map; boundary = triples on a")
    print("   boundary between its cases; leaves S = some image is not in S)")
    for n in [9, 21, 25, 45, 65, 85]:
        r = audit(n)
        notes = [f"|S| = {r['size']}", f"fixed {len(r['fixed'])}"]
        if r["boundary"]:
            notes.append(f"boundary {len(r['boundary'])}")
        if not r["maps_into"]:
            notes.append("leaves S")
        if not r["involution"]:
            notes.append("not an involution")
        found = "yes" if r["squares"] else "no"
        print(f"   n = {n}: {', '.join(notes)}; swap fixed point: {found}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact, exhaustive checks for the finitely many "
        "primes below 3000. They are evidence that each claim of the sentence "
        "is right, and the composite cases show which hypothesis each claim "
        "uses (n not a square, n prime), but they prove nothing about larger "
        "primes. Note n = 65: the argument fails (two fixed points), yet 65 is "
        "a sum of two squares - a failed proof says nothing about the truth of "
        "its conclusion. The proof for every prime is in the lesson, and Lean "
        "checks it.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Notice $n = 65 = 1^2 + 8^2$ : the argument fails, yet the conclusion holds. A failed proof says nothing about the truth of its conclusion — and a passed test says nothing about cases not tested. Only the proof covers every prime.

The second experiment treats the blueprint as a directed graph: it computes an order in which everything can be formalised, the items ready to work on now, the longest chain of dependencies (the minimum project length however many people help), and it detects a circular argument planted in a broken variant.

A blueprint as a graph: ready items, critical path, cyclesPythonExact computationComputationally tested

"""A blueprint as a dependency graph: what is ready, what is circular.

A blueprint lists the definitions and lemmas of a formalisation project and,
for each, the earlier items it uses. That makes it a directed graph, and simple
graph algorithms answer the questions a project coordinator asks every day:
which items are ready to be formalised now (everything they use is done)? In
what order can the whole project be done? What is the longest chain of
dependencies (no amount of parallel work can beat it)? And is the argument
circular somewhere (a cycle in the graph)?

The blueprint here is the one for Zagier's proof in the lesson, frozen at an
imagined moment when only some items are done. Then we break it on purpose,
letting the parity lemma "use" the oddness of |S|, and find the cycle.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import textwrap

#: Blueprint for Zagier's proof: item -> items it uses.
BLUEPRINT = {
    "def:S": [],
    "def:map": [],
    "def:swap": [],
    "lem:facts": ["def:S"],
    "lem:finite": ["def:S", "lem:facts"],
    "lem:cases": ["def:map"],
    "lem:mapsto": ["lem:cases", "lem:finite"],
    "lem:invol": ["def:map", "lem:facts", "lem:finite"],
    "lem:fixed": ["def:map", "lem:facts", "lem:finite"],
    "lem:parity": [],
    "lem:odd": ["lem:mapsto", "lem:invol", "lem:fixed", "lem:parity"],
    "thm:fermat": ["def:swap", "lem:odd", "lem:parity", "lem:finite"],
}

#: Items already formalised at the imagined moment.
DONE = {"def:S", "def:map", "def:swap", "lem:facts", "lem:finite", "lem:cases"}

def topological_order(graph):
    """Kahn's algorithm, smallest name first; None if there is a cycle."""
    remaining = {v: set(us) for v, us in graph.items()}
    order = []
    while remaining:
        ready = sorted(v for v, us in remaining.items() if not us)
        if not ready:
            return None
        v = ready[0]
        order.append(v)
        del remaining[v]
        for us in remaining.values():
            us.discard(v)
    return order

def ready_items(graph, done):
    """Items not yet done all of whose dependencies are done."""
    return sorted(v for v, us in graph.items()
                  if v not in done and all(u in done for u in us))

def longest_chain(graph):
    """A longest dependency chain (a list of items), for an acyclic graph."""
    best = {}
    for v in topological_order(graph):
        chains = [best[u] for u in graph[v]]
        best[v] = max(chains, key=len, default=[]) + [v]
    return max(best.values(), key=len)

def uses_transitively(graph, item):
    """Every item that `item` depends on, directly or indirectly."""
    seen, stack = set(), list(graph[item])
    while stack:
        u = stack.pop()
        if u not in seen:
            seen.add(u)
            stack.extend(graph[u])
    return seen

def find_cycle(graph):
    """Return a dependency cycle [v0, v1, ..., v0], or None."""
    colour = {v: 0 for v in graph}
    path = []

    def visit(v):
        colour[v] = 1
        path.append(v)
        for u in graph[v]:
            if colour[u] == 1:
                return path[path.index(u):] + [u]
            if colour[u] == 0:
                found = visit(u)
                if found:
                    return found
        colour[v] = 2
        path.pop()
        return None

    for v in sorted(graph):
        if colour[v] == 0:
            found = visit(v)
            if found:
                return found
    return None

def wrap(items, indent="   "):
    """Format a list of names in lines of at most 78 characters."""
    return textwrap.fill(", ".join(items), width=78, initial_indent=indent,
                         subsequent_indent=indent)

def main():
    order = topological_order(BLUEPRINT)
    print(f"Blueprint items: {len(BLUEPRINT)}; done so far: {len(DONE)}")
    print("A valid order in which to formalise everything:")
    print(wrap(order))
    print("Ready to formalise now (all dependencies done):")
    print(wrap(ready_items(BLUEPRINT, DONE)))
    chain = longest_chain(BLUEPRINT)
    print(f"Longest dependency chain ({len(chain)} items):")
    print(wrap(chain))
    deps = uses_transitively(BLUEPRINT, "thm:fermat")
    print(f"The theorem rests on {len(deps)} items; every item is used: "
          f"{deps == set(BLUEPRINT) - {'thm:fermat'}}")
    print()
    broken = dict(BLUEPRINT, **{"lem:parity": ["lem:odd"]})
    print("Variant in which the parity lemma 'uses' that |S| is odd:")
    print(f"   topological order exists: {topological_order(broken) is not None}")
    print("   cycle found: " + " -> ".join(find_cycle(broken)))
    print()
    print(textwrap.fill(
        "Epistemic status: exact computations on a small finite graph. They "
        "check the bookkeeping of a blueprint - order, readiness, circularity - "
        "and nothing else: a blueprint can be acyclic and complete while a "
        "lemma in it is false or its formal statement is unfaithful. That is "
        "what the formal proofs, and the people reading the statements, are for.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Exercises

1. Formalising published mathematics

Warm-upHuman

Which of the following does a blueprint for a formalisation project record? (Choose all that apply.)

Choose all that apply

An informal statement (and proof) for each definition and lemmaFor each item, the name of its formal counterpartWhich earlier items each statement or proof usesA machine-checked proof of every item

2. Formalising published mathematics

Warm-upFormal

In Lean, natural-number subtraction is truncated. What is the value of (2 : ℕ) - 5 + 4?

3. Formalising published mathematics

CoreHuman

For $p = 29$ , how many triples $(x, y, z)$ of positive integers satisfy $x^2 + 4yz = 29$ ? (This is $|S|$ .)

4. Formalising published mathematics

CoreHuman

Zagier's three cases do not cover the boundary $x = y - z$ . Which fact about $p$ shows that no element of $S$ lies on this boundary?

Choose one

p

is not a perfect square

p

is odd

p \equiv 1 \pmod 4

Nothing: the boundary case is harmless

5. Formalising published mathematics

CoreHuman

Take $n = 45 = 4 \cdot 11 + 1$ , which is not prime. How many fixed points does Zagier's map have on $S = \{(x, y, z) : x, y, z \ge 1,\ x^2 + 4yz = 45\}$ ?

6. Formalising published mathematics

CoreHuman

Someone "proves" that every $n \equiv 1 \pmod 4$ is a sum of two squares by repeating Zagier's sentence. For $n = 21$ , which claim of the sentence is false?

Choose one

"has exactly one fixed point""the finite set

S

""the involution"the parity lemma

7. Formalising published mathematics

CoreFormal

Which Lean statement faithfully formalises "every prime $p \equiv 1 \pmod 4$ is a sum of two squares"?

Choose one

∀ p : ℕ, p.Prime → p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p∀ p : ℕ, p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p∀ p : ℕ, p.Prime → p % 4 = 1 → p % 2 = 0 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p∃ p : ℕ, p.Prime ∧ p % 4 = 1 ∧ ∃ a b : ℕ, a ^ 2 + b ^ 2 = p

8. Formalising published mathematics

CoreFormal

Lean has accepted a 5,000-line formalisation of a published theorem with no sorry. Which of the following must you still check yourself? (Choose all that apply.)

Choose all that apply

That the formal statement says what the published theorem saysThat the definitions the statement uses agree with standard usageThat #print axioms shows no unexpected axiomsEvery intermediate lemma, by handThat the formal proof follows the paper line by line

9. Formalising published mathematics

StretchHuman

The formalisation of the Feit–Thompson odd order theorem (completed in 2012) is a standard example of how formal proofs relate to published ones. What did it formalise?

Choose one

A proof following later, reorganised published accounts (Bender–Glauberman 1994, Peterfalvi 2000), with new general libraries built along the wayThe 1963 paper, line by lineOnly the statement, with the proof assumed as an axiomA new proof found by computer search

10. Formalising published mathematics

StretchComputational

Write zagier_set(n), returning the sorted list of triples (x, y, z) of positive integers with x*x + 4*y*z == n, and zagier_map(t), Zagier's map with the paper's three cases. The tests check the set for small primes and that the map is an involution with the single fixed point (1, 1, k) for p = 4k + 1.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Once a result is formalised, peer review is unnecessary." The kernel checks that the formal proof proves the formal statement. Whether that statement — and every definition it uses — expresses the published theorem must still be checked by people, and so must everything a referee judges: correctness of the parts not formalised, originality, significance, exposition. Formalisation changes what reviewers need to check; it does not remove them.

Misconception

"A formal proof follows the paper line by line." Rarely. Formal proofs fill every gap, replace special arguments by general library results, and often restructure the argument — the odd order formalisation followed revised published proofs rather than the 1963 paper, and the Liquid Tensor Experiment reorganised parts of the argument as it went. Even our Zagier formalisation adds a parity lemma and a statement-conversion lemma that the sentence does not contain.

Misconception

"Lean accepted it, so the published theorem is true." Lean accepted the formal statement. A dropped hypothesis can make a statement false (and then no proof will be found); an added hypothesis can make it weaker than the published one; contradictory hypotheses make it vacuous. In the exercises you will meet a "formalisation" of Fermat's theorem that is provable precisely because it says nothing.

Misconception

"No sorry means no assumptions." A file can declare axioms, and a proof can depend on them. Always run #print axioms on the main theorems; anything beyond Lean's standard axioms must be justified and stated.

Misconception

"The kernel could be wrong, so formal proofs are no more reliable than paper ones." Kernels are small, heavily tested, and — under the de Bruijn criterion — their output can be re-checked by independent implementations. The residual risk is far smaller than the risk of an unnoticed gap in a long informal proof, though it is not zero, and honest reports say so.

ViewpointsH

Many ways of seeing

Logic— What exactly has been verified

A formal proof shows that a sentence is derivable in a specific formal system — for Lean, a dependent type theory (the calculus of inductive constructions with a hierarchy of universes, quotients and the axiom of choice). That system is stronger than ZFC: its universes behave like inaccessible cardinals, and its consistency strength is roughly that of ZFC with one inaccessible cardinal for each universe (Werner 1997; Carneiro 2019). By Gödel's second incompleteness theorem no such system proves its own consistency, so "verified" always means "derivable in a system we have good reason to believe consistent". In practice the theorems of ordinary mathematics use far less than the system offers, and the question of which axioms a proof uses — visible through #print axioms — is a question of logic that formalisation makes precise. See type theory and large cardinals.

Number theory— Two proofs of one theorem

Zagier's proof is combinatorial; Mathlib's proof of Nat.Prime.sq_add_sq is algebraic: in the Gaussian integers $\Z[i]$ , a Euclidean domain, a prime $p \equiv 1 \pmod 4$ divides $m^2 + 1 = (m + i)(m - i)$ for some $m$ (as $-1$ is a square mod $p$ ), but divides neither factor, so it is not prime in $\Z[i]$ and factors as $p = (a + bi)(a - bi) = a^2 + b^2$ . The algebraic proof generalises to the arithmetic of number fields and binary quadratic forms (algebraic number theory); the combinatorial one gives a different kind of insight — a parity — and was much faster to formalise from scratch. Large number-theory formalisations, such as the ongoing project on Fermat's Last Theorem, must build the algebraic route at full strength: modular forms, Galois representations, deformation theory.

Combinatorics— The involution principle and fast formalisation

The parity lemma is an instance of a general combinatorial principle: an involution pairs off the non-fixed elements, so $|A| \equiv |\mathrm{Fix}(f)| \pmod 2$ ; more generally, when a group of order $p^n$ acts on a finite set, the number of fixed points is congruent to the number of elements modulo $p$ (Mathlib's MulAction.card_modEq_card_fixedPoints). Such finite, explicit arguments formalise well, which is one reason combinatorics has seen spectacular formalisations: the four colour theorem, and the proof of the polynomial Freiman–Ruzsa conjecture, which went from preprint to complete Lean proof in weeks (see additive combinatorics) because its blueprint split it into many short, independent lemmas that dozens of contributors could take on in parallel.

Geometry— When the referees could not finish

The Kepler conjecture — no packing of equal balls in $\R^3$ has density greater than $\pi/\sqrt{18}$ — was proved by Hales by reducing it to a finite but enormous problem: a list of candidate local configurations, each eliminated by linear programming and interval arithmetic. The human-readable part could be refereed; the computational part could not be checked line by line by people. Flyspeck formalised both, turning a proof that was "99% certain" in the referees' judgement into one checked by a kernel. Geometry also shows the statement problem sharply: "packing" and "density" have to be defined for infinite configurations, and the formal definitions had to be checked against the classical ones.

Topology— Formalising the h-principle

Smale's theorem that a sphere can be turned inside out through immersions is a consequence of Gromov's h-principle: for open ample differential relations, every formal solution can be deformed to a genuine one. The proof by convex integration is analytic and geometric, with many estimates that informal accounts treat lightly. Its formalisation by van Doorn, Massot and Nash required differential topology that Mathlib lacked (smooth manifolds, parametric constructions, homotopies of maps) and showed that blueprints work as well for continuous, estimate-heavy mathematics as for algebra. See differential topology.

Category theory— Statements that live in a category of sheaves

The Liquid Tensor Experiment's main statement concerns Ext groups computed in the category of condensed abelian groups — sheaves of abelian groups on the site of profinite sets. Even stating it formally required a large slice of category theory (abelian categories, derived functors, sheaves on a site with a size-controlled set of covers) and careful handling of universe levels, since condensed sets involve "all profinite sets". It is a case study in how much infrastructure a faithful statement can require, and in why libraries matter: the infrastructure built for one project becomes part of everyone's foundations. See sheaves.

History & global context

History and context

Automath and Mizar. Nicolaas Govert de Bruijn began the Automath project in Eindhoven in 1967; L. S. van Benthem Jutting formalised Landau's Grundlagen der Analysis in it (1977). Andrzej Trybulec started Mizar in Poland in 1973; its Mizar Mathematical Library, built over decades in Białystok and elsewhere, was for a long time the largest body of formalised mathematics.
LCF, HOL, Coq, Isabelle. Robin Milner's LCF (1970s) introduced the design in which only a small kernel can create theorems. Descendants include HOL Light (John Harrison), Isabelle (Lawrence Paulson, 1986), and Coq (Thierry Coquand and Gérard Huet, from 1984, now called Rocq), based on the calculus of constructions.
Lean and Mathlib. Leonardo de Moura started Lean at Microsoft Research in 2013; Lean 4 (de Moura and Sebastian Ullrich, 2021) is both a proof assistant and a programming language. The community library mathlib began in 2017 and was ported to Lean 4 as Mathlib in 2023. Its contributors work in dozens of countries.
Milestones. Four colour theorem (2005), odd order theorem (2012), Kepler conjecture (2014), Liquid Tensor Experiment (2022), polynomial Freiman–Ruzsa conjecture (2023). Freek Wiedijk's list of "100 theorems" has tracked for two decades which famous theorems each system has formalised.

One sentence, and a challenge

Three layers and a bridge

Definitions

A blueprint for Zagier's sentence

The proof, with nothing left out

Large formalisations: what they did and did not verify

Zagier's proof in Lean

Testing before proving, and managing the blueprint

Exercises

Common misconceptions

Many ways of seeing

History and context

Further reading