%======================================================================
\section{Reproduction}\label{s:stats}

The Lean archive of [repo] is a git archive of the release files of a commit that differs from the audited commit \lean{e8e86d3} only in its
README. The archive pins Lean \lean{v4.35.0-rc3} and Mathlib at
commit \lean{c55e6e786f49}. With \lean{elan} installed, the three commands of its README, \lean{lake exe cache get},
\lean{lake build U1} and \lean{lake env lean PrintAxioms.lean}, fetch the Mathlib build for the pinned commit, build the
library and print the statements and axioms of the theorems of Theorem~\ref{thm:formal}. A clean
build of the library took $382$ seconds of wall-clock time on a 60-core machine, with a peak of $3.7$\,GiB in its largest
process. The release checks were run on \lean{e8e86d3}, and their report
\lean{release-checks-e8e86d3.md} in [repo] gives the figures of the checks not given here. The audit reports in
\lean{audit/} describe earlier commits, most recently \lean{254a4d3} and \lean{1873b51}, whose library, with comments
removed, is that of \lean{e8e86d3}.