The Lean verification bundle — machine-checked claims

Every claim in the Principia articles carrying the Lean label is machine-checked in Lean 4 + mathlib. The complete sources are distributed here — the bundle, how to check it, the ledger of theorems, and the bundles in preparation.

Related: Taking stock of novelty (the sorting of results) / What remains / certificates for k=4 / certificates for Lovász

The contents and sha256 of this bundle are fixed. New theorems are distributed as separate bundles (§04).

tar -xzf shioriproofs-src.tar.gz
cd shioriproofs
./verify.sh

verify.sh decides the degree of parallelism from the machine's RAM and CPU count, runs lake exe cache get (mathlib's prebuilt cache) and lake build Shioriproofs.ChkAll, retries the same command if it falls over (up to 6 times), and finally summarises the axiom output and the counts of sorryAx and Lean.ofReduceBool. By hand, it comes to the same as this:

# parallelism: 1 for 3 GB of RAM, 4–6 for 16 GB
lake exe cache get
LEAN_NUM_THREADS=1 lake build Shioriproofs.ChkAll

ChkAll.lean is nothing but a list of #print axioms for the 27 headline theorems. Building it prints the axioms each theorem depends on. [propext, Classical.choice, Quot.sound] are the three standard axioms of Lean / mathlib, and neither sorryAx (an unproved hole) nor Lean.ofReduceBool (native_decide) appears for any of the 27.

Why the parallelism is limited. A single proof uses up to 1.5–2 GB of memory. Lake's default builds as many files at once as there are CPUs, so on a 3 GB machine four at once fall into swap and neither fail nor progress. Lake 5 has no -j, so LEAN_NUM_THREADS is used instead. Lake resumes from where it left off.

The full name of each theorem (with namespace) and the file and line where its proof is written. An empty axiom column means the three standard axioms.

Erdős problem #169 (28 theorems, 20 of them headline)

Two names do not match their file names — Shiori844.Blk_apfree is in Erdos844a.lean and Shiori814.record_3_00849 in Erdos815d.lean. Erdos834c.lean also holds a primed theorem record_3_00849'; ChkAll looks at the unprimed one. Part of the 110-level lower bound (Erdos1105c) peaks at 9.34 GiB RSS and will not build on a 3 GB machine. The lower bound inside Lean for the 84 levels is 3.0085385 (not the Python bracket 3.008538522178).

The Collatz conjecture (7 theorems)

Theorems machine-checked outside the bundle of §01. Each group is being prepared for distribution in a store of its own — the URL and sha256 will be written here when it is placed. The count under "axiom output" is the number of declarations that the group's Chk*.lean lists with #print axioms; all of them use at most the three standard axioms, with no sorryAx and no Lean.ofReduceBool. Only groups whose axiom output is at hand are listed with a count; the others are marked "not yet on file".

Notes for a third-party build (bundles in preparation). These have been built only on the machine where the proofs were written (15 GiB of RAM). Build one file at a time (building a Chk* in one go lets lake run the heavy files in parallel, which falls over even with 15 GB). Peak RSS is about 11.8 GiB (the GP(n,3) counts), about 10 GiB for the def = 2 group, and about 6.7 GB for the general-n group of GP(n,3). Allow 12 GB of RAM or more. The certificates are "the shape of a tree and integer bounds only"; the boxes are computed by Lean.

For the bundle of §01, a writer other than the one who wrote the proofs ran lake build Shioriproofs.ChkAll on the same sources and confirmed:

• the build completed with 0 errors (3,036 jobs)
• the axiom output of all 27 theorems matches the ledger above
• 0 occurrences of sorryAx, 0 of Lean.ofReduceBool (no native_decide)

The bundle itself (the tar.gz) was also run from scratch by the official procedure (./verify.sh) on a separate machine with 3 GB of RAM, 2 cores and 4 threads, and completed — the 31 modules ChkAll depends on built with 0 errors and 0 out-of-memory events in 9 hours 13 minutes, and the axiom output of the 27 headline theorems matches the ledger. The slow parts are specific modules that shut a 5–6 GB computation into the kernel with decide, each taking 2–3 hours. This is the basis for recommending 8 GB or more. A subsequent ./verify.sh --all built the remaining modules that ChkAll does not depend on, confirming that every module of the bundle produces its olean (a little over 13 hours in all from scratch).

These are re-runs on a single machine, not a replication across hardware. Replication in another environment is exactly what this distribution is for — if your results differ, please say so via Contact.

One failure on the side of checking also turned up while preparing this distribution. The axiom list was at first counted by the string "depends on axioms", giving 26 theorems. There are 27 — Shiori793.chain_verified alone uses no axioms at all, and its output is the different phrase "does not depend on any axioms", so it slipped through the counting check. The strongest theorem of all was invisible to a check that counts axioms. When you write a check, try to fool it.

A machine check guarantees that the conclusion follows from the proposition as written. Whether the proposition says what was intended, and whether it is new, the machine does not say. That sorting is in Taking stock of novelty.