The Lean verification bundle — the ledger of machine-checked claims

Every claim in the Principia section that carries the Lean label has been checked by machine in Lean 4 with Mathlib. The complete sources are here, and you can rebuild them yourself. There is one bundle, divided into namespaces by topic.

Related: The Lean guide (what a machine check is, and how to run one) / Papers / Taking stock of novelty / What remains / Certificates for the Lovász conjecture

The previous version principia-src.tar.gz (sha256 131d8da3426838ca…, of 2026-09-25) is cited by papers and forum posts, so it stays in place with its URL and sha256 unchanged; the new version adds the deficiency-2 and GP(n,3) modules on top of it and leaves the existing modules the same. Bundles distributed earlier remain in place with their URLs and sha256 unchanged. Their theorems are the same as in this bundle; only the namespaces and file names differ. For a fresh check, use this bundle.

Bundles by article

Bundles holding only the modules of one topic, one per article or paper. lakefile.lean, lake-manifest.json and lean-toolchain point to the same environment as the bundle above, and the .lean files are identical. Each bundle carries its own axiom log (axioms-<bundle>.txt).

The 2026-10-01 version of the GP(n,3) bundle (sha256 45b896c0…) has a doubled import prefix in its entry file Principia.lean, so lake build fails on it (the modules can still be built by name). It stays at its URL unchanged; the 2026-10-02 version above has identical .lean files and only the entry file corrected.

tar -xzf principia-src-2026-10-01.tar.gz
cd principia
lake exe cache get                        # Mathlib's prebuilt cache
LEAN_NUM_THREADS=1 lake build Principia

Principia.lean is an entry point that only imports every module. Restrict the build to one thread. Some proofs shut computations of several GB up to 12 GiB inside the kernel; lake's default is to build as many modules in parallel as there are CPUs, and even a 16 GB machine will swap with four at once. lake resumes from where it left off.

To rebuild a single module, name it.

LEAN_NUM_THREADS=1 lake build Principia.APFree.BellmanRecord

At the end of each module there is a #print axioms for the main theorems it declares; building prints the axioms each theorem depends on. [propext, Classical.choice, Quot.sound] are the three standard axioms of Lean and Mathlib; neither sorryAx (an unproved hole) nor the axiom added by native_decide appears anywhere. The bundled axioms-principia.txt is the full output from our build. For a step-by-step reading, see chapter 09 of the Lean guide.

For each namespace: the number of files, the main theorems with their locations, the axiom status, and the article they come from. The full name of a theorem is <namespace>.<theorem>; the location is the file and line inside the bundle. The list of every module and the sha256 of each file is in the bundle's README.md.

Theorems that are machine-checked outside the bundle above. They are being prepared for distribution as bundles; the URL and sha256 will be written here when they are placed. The paper drafts are on the Papers page.

These have only been built on the machine the proofs were written on (15 GiB of RAM). Build them one at a time. The largest resident size is about 11.8 GiB (the GP(n,3) count), about 10 GiB for the deficiency-2 bundle.

The bundle of §01 was made by rebuilding all 225 modules one at a time in dependency order (the 2026-10-01 version adds the 9 modules for deficiency 2 and GP(n,3)).

• 0 errors, 0 sorry, 0 native_decide
• 3,149 lines of axiom output, every line a subset of the three standard axioms
• The declaration names and their axioms agree, as sets, with the output of the version before the namespaces were renamed
• With comments stripped, the bodies are identical to the earlier version except for the import lines
• The 100 modules for #827 were also re-checked in a version rebuilt independently from the originals

This is a re-run on the same machine, not a replication across hardware. Replication elsewhere is exactly what this distribution is for — if your result differs, tell us through the contact page.

2026-10-02 — rebuilding from the distributed bundles

Each distributed bundle was unpacked into a fresh directory, apart from the working tree in which the proofs were written, and built from its own contents alone: lake exe cache get, then LEAN_NUM_THREADS=1 lake build. The #print axioms output of each build was compared line by line with the axiom log shipped in the bundle.

• principia-riemann-weil-form-2026-10-02 — 12 files, 0 errors, 73 axiom lines identical to the shipped log
• principia-generalized-petersen-2026-10-02 — 7 files, 0 errors, 185 axiom lines identical to the shipped log
• principia-hodge-cm-degenerate-2026-10-02 (first version) — all 46 files built and the 945 axiom lines were identical to the shipped log; but loading the entry file Principia.lean stopped on a clash of auto-generated instance names between CMHodgeClasses and CMHodgeDegenerate. The distributed c version leaves that one module out of the entry file (the modules themselves are unchanged)
• principia-src-2026-10-01 (the bundle above) — 223 files, 0 errors, 3,110 axiom lines identical to axioms-principia.txt. About ten hours
• principia-hodge-cm-degenerate-2026-10-02c (the distributed version) — all 46 files and the entry file built, 0 errors, 945 axiom lines identical to the shipped log

The builds ran on the same laptop on which the proofs were written (the server behind this site has too little memory). They are rebuilds from the distributed sources, not a replication across hardware.

A machine check guarantees that the stated proposition follows from the proof. Whether the proposition says what was intended, and whether it is new, the machine says nothing about. That sorting is in Taking stock of novelty and in chapter 08 of the Lean guide.