Formalising published mathematics

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

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

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

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?

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\}$?

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?

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

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.)

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?

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.