Proof by exhaustion: one plus one is two, in 616,873 lines of Lean

We formalise the proposition 1 + 1 = 2 in the Lean 4 proof assistant, with no library and without Lean's built-in natural numbers, integers or rationals. The proposition is proved in a deep embedding of a Hilbert-style calculus with a proved soundness theorem, in Peano numerals, von Neumann ordinals and Church numerals, in the integers and rationals built as quotients, in the reals built as Cauchy sequences of rationals, in the complex numbers, quaternions and octonions built by the Cayley–Dickson doubling, in binary numerals with a proved ripple-carry adder, in the integers modulo n for every n from 2 to 500, in two Roman notations, in an addition table, and along a chain of 99,999 lemmas ending in 100,000 − 99,998 = 1 + 1. On the way the development proves that 0.999… = 1, that 0.999… + 1.999… ≠ 2, that multiplication of quaternions is not commutative, and that multiplication of octonions is not associative. A final theorem, numbered ✱54.46 after Whitehead and Russell, collects every result. The tree has 616,873 lines of Lean, of which 7,493 are written by hand, with 101,708 theorems and 100,714 definitions. Every theorem is used in the proof of another or cited by the final theorem, no two theorems have the same statement, and both facts are checked by a program that runs inside Lean. The only axioms used are propext, Quot.sound and, through the soundness theorem of the embedded calculus only, Classical.choice.