A Formalization at Large —— Laver Function in Lean

The Laver function $F(n)$ is a fast-growing function that can be defined by the following concise code:

def l(n,a,b):return b if a==1<<n else a+1 if b<2 else l(n,l(n,a,b-1),a+1)

def F(n,m=1):
 k=1
 for _ in range(n):k=l(m,1,k)
 return m-1 if k-(1<<m) else F(n,m+1)

One may easily compute its initial values: $ F(0) = 0 $, $ F(1) = 1 $, $ F(2) = 2 $, $ F(3) = 4 $. However, $F(4)$ is already an extremely large number, far too large to be represented or stored by any computer system. Despite its simple, combinatorial definition, the study of this function involves the strongest large cardinal axioms known to mathematics. Richard Laver first defined this function in 1992¹ in his study of Laver tables. In the next year, Dougherty² gave a lower bound for its growth rate, but the bound was weaker than Graham’s function. For over 30 years, no progress was made on this lower bound.

The growth rate of a computable function is limited by the strength of the axiomatic system required to prove its totality—that is, to prove that the program halts for every natural number input. For example, if a computable function’s totality can be proven in Peano Arithmetic (PA), then its growth rate must be below $ f_{\varepsilon_0}(n) $ where $f$ denotes the fast-growing hierarchy. However, the only known proof of the Laver function’s totality requires the large cardinal axiom I3, one of the strongest axioms known in set theory, suggesting an enormous potential growth rate.

In his 1993 paper², Dougherty asked whether one could prove that the Laver function grows faster than $ f_{\varepsilon_0}(n) $, thereby showing its totality is unprovable in PA. In the same paper, he proved that the strongest asymptotic lower bound was only around $ f_{\omega+1} (n) $, still well below the target.

The simplicity of the problem, together with its deep ties to the strength of the axiomatic systems, has made it a topic of considerable interest. For further exposition of this problem, see John Baez’s blog post Shelves and the Infinite³, a short MathOverflow answer⁴, and Chinese-language Zhihu answers by @费事发财⁵, @Achatinidae⁶ and Qi himself⁷. The problem has long been considered difficult. Randall Dougherty (an IMO medalist with 1 gold and 2 silver)⁸ and Thomas Jech further studied it⁹ but did not resolve it. Patrick Dehornoy frequently mentioned the problem in many articles and books. Finally, in 2025, Renrui Qi (also an IMO gold medalist)¹⁰ achieved a decisive breakthrough by solving it with techniques from googology¹¹, an area of recreational mathematics dedicated to the study of large numbers.

About Googology

The term googology combines googol, meaning $10^{100}$ or 1 followed by 100 zeros, with the suffix -ology, meaning “the study of”. Reflected by its name, googology begins with a simple question: How can we define an extremely large but still finite number? Of course there is no largest integer—any number can always be increased by 1—the subject becomes an open-ended search for increasingly powerful ways to describe large numbers. This typically involves introducing a notation, recursive rule, or mathematical structure, then studying how rapidly it grows and how it compares with other systems.

Ordinary exponentiation soon becomes inadequate. Exponent towers, Knuth’s up-arrow notation, and Conway’s chained-arrow notation lead naturally to recursive functions, fast-growing hierarchies, ordinal notation systems, combinatorial constructions, and even uncomputable functions. Graham’s number, TREE(3), and various fast-growing hierarchies are among the best-known objects discussed in googology.

Googology is primarily a form of recreational mathematics and enthusiast-driven mathematical culture. Many of its contributors are not professional mathematicians; they develop new large-number notations, compare growth rates, and search for stronger constructions. At the same time, pushing the question of “how large can we go?” far enough naturally brings the subject into contact with deeper areas of mathematics. Comparing extremely fast-growing functions leads to computability theory; asking which axiomatic systems can prove that such functions are total leads to proof theory; and constructions involving transfinite ordinals, independence phenomena, or large cardinals enter the territory of set theory.

This is part of what makes googology distinctive: it begins with an almost childlike question—“Can I write down a larger number?”—but, when pursued far enough, it reaches fundamental questions about computation, proof, infinity, and the limits of formal mathematical systems. It is from this soil that Qi’s proof technique emerges.

About Qi’s Proof

Before formalization, Qi’s paper had already gone through four versions, the final one running to 42 pages. The proof draws its technique largely from googology. Qi introduced a large-number notation called the basic Laver pattern (blp). One can define a fast-growing function hierarchy $f(p, n)$ for every blp term $p$ and natural number $n$. The proof has two parts:

1. Comparing the Laver function $F(n)$ with $f(p, n)$. This part proceeds through the construction of a basic Laver system (bls), assigning ordinals to nodes in a blp in order to establish its relation to the Laver function.
2. Ordinal analysis comparing $f(p, n)$ with $f_{\varepsilon_0}(n)$. This is a routine technique from googology. Note that the exposition in the paper is still far from making full use of the ordinal analysis of blp; a much stronger growth-rate result should be provable with a more thorough ordinal analysis of blp.

The result is significant, but the proof is long, combinatorially dense, and draws on techniques from googology that lie outside the training of most logicians and set theorists. Referees who combine the set-theoretic academic background with the googological machinery are not readily available. Under these conditions, conventional peer review is slow and and perhaps impracticable, making formalization the most credible path to independent verification.

The Formalization

Professor Liang Yu of Nanjing University noticed this work and reached out to the PKU team, believing it to be an important contribution and asking whether it could be formalized in order to verify it. The PKU team accepted this task, which aligns with one of the central aims of formalization: to verify a proof whose correctness is uncertain and to help mathematicians review and understand it.

Zhiyuan Zhang completed the entire formalization, refining dedicated agents for human–AI collaboration based on Opus 4.8 throughout the process. The AI first expanded and paraphrased the proof from the manuscript, then carried out the formalization, during which there was extensive human–AI interaction in all directions. For example, human–AI collaboration jointly identified and discussed subtle mathematical points in the paper, while human promptly steered the AI’s formalization in the right direction. This process helped Zhiyuan accumulate experience in refining the formalization pipeline and in building larger formalization repositories later, such as FormalPantheon¹², a formalized collection of important and elegant mathematical results.

In this project, the following result from Qi’s paper, together with all its dependencies, has been formalized sorry-free and has passed the comparator’s check.

Suppose the I3 axiom holds. Then the Laver function $F(n)$ grows faster than $f_{\varepsilon_0}(n)$, and thus its totality cannot be proved in PA.

The formalization depends on two upstream mathematical libraries, Mathlib¹³ and Foundation¹⁴. The first version of the repository contained 80k lines of code; its quality was later improved, reducing the published repository to 36k lines of code.

Several difficulties had to be overcome during formalization. One major source was that certain definitions required adjustment. None of these were fatal errors, and, as expected, formalization brought all of them to light. However, because they occurred in newly introduced combinatorial definitions from googology, understanding how to fix them remained difficult. Another was that neither Mathlib nor Foundation yet provides comprehensive support for PA-provability and related infrastructure, so we formalized these ourselves. We also included an independent formalization component concerning the classical equivalence between PA-provability and growth rate $\le f_{\varepsilon_0}(n)$¹⁵.

In completing the formalization of the entire project, we also obtained a revised version of the paper’s proof. Although some minor errors were found, in a proof of this length and combinatorial density such issues are not unusual, and none of them affect the main proof strategy. We fixed all of them and compiled our findings into a detailed report¹⁶, which we sent to Qi. After receiving our report, Qi revised his paper and updated arXiv to v5 two weeks later, incorporating our corrections and clarifications. Ultimately, the formalization effort and the feedback exchanged with Qi contributed to the mathematical content of the paper.

Beyond Formalization

The main formalization work was carried out between April 6 and June 11, and the report was completed on June 17. This project provides a concrete case: a cross-domain result with no natural referee pool was independently verified and corrected through formalization within two months. The conditions under which formalization offers this advantage are specific: the result is significant enough to justify the effort, the proof is long and combinatorially dense, and domain expertise is scarce. When all three hold, formalization may be the most credible verification path available.

Qi’s work, which applies techniques from googology back to mathematical logic, is of distinctive significance. This is not an end but a beginning of absorbing techniques from googology to mathematical logic. Even in this paper, there remain ordinal analysis techniques that can be further improved. We would be delighted if our work could play some small part in advancing the techniques of googology and their application to mathematical logic and other branches of mathematics. We also hope our work can provide some groundwork for the formalization of googology.

A fun note: In the remaining part of Qi’s paper, he defines a large-number notation called the Laver table yarn (LTY). According to Qi, this is potentially the strongest recursive notation for ordinals ever to have appeared in human mathematical history—apart from the kind that cheats using provability. Although it is not used in the main proof, we formalized this part as well after the main proof. It would be a remarkable delight if we had truly formalized the strongest recursive notation for ordinals—or, equivalently in some sense, the largest computable natural number notation ever to have appeared in the history of mathematical research.