Laver Table

A standalone Lean 4 formalization of Theorem 1.1 from Renrui Qi's Notes on Laver Tables:

Laver's function F dominates every computable function whose totality is provable in Peano Arithmetic.

The report written during the formalization are summarized in LaverTableReport.pdf and discussed in an accompanying blog post.

Comparator/Statement.lean defines the set-theoretic language, VSet lam, the I3 hypothesis, critical points, the critical sequence, application, Iter(j), crit*(j), Laver's function, PA-provable totality, and eventual strict domination. The proof is assembled in LaverTables/Main.lean.

References

• [Qi25] Renrui Qi, Notes on Laver Tables, arXiv:2501.06733v4, 2025.
• [Lav92] Richard Laver, On the Algebra of Elementary Embeddings of a Rank into Itself, arXiv:math/9204204, 1992.
• [Dou92] Randall Dougherty, Critical Points in an Algebra of Elementary Embeddings, arXiv:math/9205202, 1992.
• [DJ92] Randall Dougherty and Thomas Jech, Finite Left-Distributive Algebras and Embedding Algebras, arXiv:math/9209202, 1992.
• [Dou95] Randall Dougherty, Critical Points in an Algebra of Elementary Embeddings, II, arXiv:math/9503204, 1995.
• [Dim17] Vincenzo Dimonte, I0 and Rank-Into-Rank Axioms, arXiv:1707.02613, 2017.
• [Wei06] Andreas Weiermann, Classifying the Provably Total Functions of PA, Bulletin of Symbolic Logic 12 (2006), 177-190, author PDF.

Build and Trust

The project uses Lean and Mathlib v4.31.0; all dependencies are pinned by lake-manifest.json.

LaverTables.I3 is the proposition asserting the existence of a nontrivial elementary self-embedding of some limit stage VSet lam. It is an explicit hypothesis of the main theorem. Note that we should not expect the I3 axiom, a large-cardinal axiom of consistency strength far beyond the existence of countably many inaccessible cardinals, to be derivable from Lean's underlying type theory alone.

Comparator

The Comparator/ directory follows the leanprover/comparator:

• Challenge.lean imports the statement surface and replaces the proof by a hole.
• Solution.lean supplies the formalized proof under the same declaration name and type.
• config.json permits only Lean's kernel axioms; the challenge theorem takes I3 as an explicit premise.

Use comparator and lean4export release v4.31.0:

COMPARATOR_LANDRUN=/path/to/landrun \
COMPARATOR_LEAN4EXPORT=/path/to/lean4export \
lake env /path/to/comparator Comparator/config.json

Nanoda checking is disabled in Comparator/config.json; the exported solution is still replayed by Lean's kernel.