The Lumenary · Research pathways

Formalising published mathematics

Name: ______________________

Date: ______________________

You will learn to

Write a blueprint that breaks a published theorem into formalisable definitions and lemmas and records their dependencies
Formalise a short published result — Zagier's one-sentence proof of Fermat's two-squares theorem — recording every gap and implicit assumption found along the way
Identify the trusted base of a formal proof and check that a formal statement faithfully captures the published theorem
Describe completed large formalisations, such as the odd order theorem, the Kepler conjecture and the Liquid Tensor Experiment, and what they did and did not verify
Contribute to a large library such as Mathlib, and work in a collaborative formalisation project

1.
Which of the following does a blueprint for a formalisation project record? (Choose all that apply.)
- A.An informal statement (and proof) for each definition and lemma
- B.For each item, the name of its formal counterpart
- C.Which earlier items each statement or proof uses
- D.A machine-checked proof of every item
2.
In Lean, natural-number subtraction is truncated. What is the value of (2 : ℕ) - 5 + 4?
3.
For $p = 29$ , how many triples $(x, y, z)$ of positive integers satisfy $x^2 + 4yz = 29$ ? (This is $|S|$ .)
4.
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?
- A. $p$ is not a perfect square
- B. $p$ is odd
- C. $p \equiv 1 \pmod 4$
- D.Nothing: the boundary case is harmless
5.
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.
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?
- A."has exactly one fixed point"
- B."the finite set $S$ "
- C."the involution"
- D.the parity lemma
7.
Which Lean statement faithfully formalises "every prime $p \equiv 1 \pmod 4$ is a sum of two squares"?
- A.∀ p : ℕ, p.Prime → p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p
- B.∀ p : ℕ, p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p
- C.∀ p : ℕ, p.Prime → p % 4 = 1 → p % 2 = 0 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p
- D.∃ p : ℕ, p.Prime ∧ p % 4 = 1 ∧ ∃ a b : ℕ, a ^ 2 + b ^ 2 = p
8.
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.)
- A.That the formal statement says what the published theorem says
- B.That the definitions the statement uses agree with standard usage
- C.That #print axioms shows no unexpected axioms
- D.Every intermediate lemma, by hand
- E.That the formal proof follows the paper line by line
9.
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?
- A.A proof following later, reorganised published accounts (Bender–Glauberman 1994, Peterfalvi 2000), with new general libraries built along the way
- B.The 1963 paper, line by line
- C.Only the statement, with the proof assumed as an axiom
- D.A new proof found by computer search
10.
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.
Computational — Practice

Answer key — Formalising published mathematics

1.
A blueprint records informal statements and proofs, links each item to its formal counterpart, and records the dependency relation. The formal proofs themselves are in the proof assistant; the blueprint tracks which of them are done.
2.
2 - 5 = 0 in ℕ, so (2 : ℕ) - 5 + 4 = 4. This is why Zagier's $x - y + z$ is written x + z - y in the formalisation: the two agree only when $x \ge y$ , and on $S$ the second is the right one.
3.
$x = 1$ : $yz = 7$ , giving $(1, 1, 7)$ and $(1, 7, 1)$ . $x = 3$ : $yz = 5$ , giving $(3, 1, 5)$ and $(3, 5, 1)$ . $x = 5$ : $yz = 1$ , giving $(5, 1, 1)$ . So $|S| = 5$ , which is odd, as Zagier's argument predicts. The fixed point of Zagier's map is $(1, 1, 7)$ , and the fixed point of the swap is $(5, 1, 1)$ , giving $29 = 5^2 + 2^2$ .
4.
If $y = x + z$ then $x^2 + 4yz = x^2 + 4xz + 4z^2 = (x + 2z)^2$ , a perfect square. A prime is not a perfect square, so the boundary never occurs on $S$ . For $n = 9 = 1^2 + 4 \cdot 2 \cdot 1$ it does occur, at $(1, 2, 1)$ .
5.
A fixed point has $x = y$ and $x(x + 4z) = 45$ with $z \ge 1$ . $x = 1$ : $z = 11$ . $x = 3$ : $3 + 4z = 15$ , $z = 3$ . $x = 5$ : $5 + 4z = 9$ , $z = 1$ . So there are three fixed points, $(1, 1, 11)$ , $(3, 3, 3)$ and $(5, 5, 1)$ ; the claim "exactly one fixed point" uses primality. (Here $|S| = 7$ is still odd, and indeed $45 = 3^2 + 6^2$ — but the argument no longer proves it.)
6.
For $n = 21$ the map is still an involution of the finite set $S$ , but it has two fixed points: $21 = 1 \cdot 21$ gives $(1, 1, 5)$ and $21 = 3 \cdot 7$ gives $(3, 3, 1)$ . So $|S| = 4$ is even and nothing follows. The step "exactly one fixed point" is where primality is used.
7.
Only the first statement has exactly the theorem's hypotheses (prime, $\equiv 1 \pmod 4$ ) and conclusion, quantified over all $p$ . The second is false, the third is vacuously true, and the fourth is an existential statement that is far weaker. A kernel will happily check a proof of the third or fourth — which is why people must read formal statements.
8.
The trusted base is the kernel, the axioms used and the formal statement with its definitions. So you must check the statement and its definitions against the paper and inspect the axioms. The intermediate steps are checked by the kernel, and the proof need not follow the paper.
9.
The odd order formalisation (Gonthier and collaborators, Coq and Mathematical Components) followed the revised proofs of Bender and Glauberman and of Peterfalvi, not the 1963 paper line by line, and built libraries of finite group theory and character theory. It verified the theorem, not the original text.

10.

def zagier_set(n):
    triples = []
    x = 1
    while x * x < n:
        rest = n - x * x
        if rest % 4 == 0:
            m = rest // 4
            triples += [(x, y, m // y) for y in range(1, m + 1) if m % y == 0]
        x += 1
    return sorted(triples)


def zagier_map(t):
    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)

The tests are evidence for seven primes. The lemmas in the lesson (and the Lean proofs) show the same properties for every prime $p \equiv 1 \pmod 4$ .