What It Actually Costs to Name a Huge Number

Years ago I wrote a couple of pieces here trying to get a handle on infinity (Hilbert's Hotel, the different sizes of it, that kind of thing). This is a spiritual sequel, except the number in question isn't infinite. It's finite, perfectly well-defined, and still almost impossible to hold in your head, because it's defined not by counting but by description: the biggest number you can pin down with a fixed budget of symbols. Big numbers are an old interest of mine; Graham's number, Rayo's number and most of the rest of the canon have been rattling around my head for years. What set this project off was two CodeParade videos on the "biggest number in a fixed message length" game: digits, power towers, Graham's number, increasingly compact programming languages, and finally Rayo's number at the top of the ladder. The videos didn't introduce me to any of these numbers. What they sparked was a specific itch the game itself never scratches: how do you specify a big number rigorously, in the smallest amount of space? That itch sent me down a rabbit hole that ended, a couple of days later, with me and a small army of coding agents mechanically verifying pieces of formal logic that, as far as I can tell, nobody had written down before.

The actual question

"Biggest number in N symbols" isn't quite a well-formed question on its own: it depends entirely on the rules you're allowed to use to write the description. So the real question is two-dimensional: fix a system of rules R (a grammar plus a way of evaluating expressions), and ask what number you can name with a budget of n symbols. Call that BN(R, n). But R itself has to be specified somehow, and specifying more powerful rules costs more up front. Call that cost κ(R). The question that actually interested me: does growth rate scale predictably with how much you pay for the rules, or is it something messier?

I ran an autonomous build loop across six real systems (Turing machines, binary lambda calculus, the Bashicu Matrix System in both its single-row and multi-row forms, System F, and first-order set theory, Rayo's own family), pricing κ(R) in a common unit and reading off how fast BN(R, n) grows for each. No clean law. Once a system is Turing-complete, it hits uncomputable growth within a few hundred bits and paying more buys nothing faster. Only the systems that stop short of full Turing-completeness, the ones indexed by an ordinal instead, show a real gradient, and even that might just be the sequence people happened to formalize rather than a genuine law.

Naming zero through six, the hard way

Rayo's own row in that table came back "infeasible to pin down exactly." So I went and pinned it down, by mechanically proving in Lean 4 exactly how many symbols it costs to name the numbers 0 through 6, using nothing but first-order set theory: membership, logic connectives, quantifiers. No numerals. No arithmetic. You want to say "zero," you have to describe the empty set from scratch.

The numbers: 10, 30, 128, 403, 1228, 3703, 11128. A ratio that settles to almost exactly 3x per step and stays there. That's a genuinely brutal rate for something as modest as counting to six, and it's suspicious for a different reason: if that rate holds forever, a googol-symbol budget (Rayo's actual number uses one) only reaches somewhere around the 200th number. That's nowhere close to the reputation.

The resolution is that the strategy I'd mechanized ("x's members are exactly 0, 1, 2, ... k-1, list them all out") is close to the worst possible one. It's unary counting wearing a tuxedo. Chasing that down properly, a successor-chain naming (just count up to six, reusing the same "successor of" step each time instead of re-deriving every earlier number from scratch) costs 388 symbols for the same target: 28.7x cheaper, also mechanically verified. Real number, not an estimate.

But even that isn't the actual trick. Every strategy above, cheap or expensive, builds its number up from the empty set, and in first-order set theory it has to, because a number is the set of its predecessors and the language gives you nothing but membership and logic to describe it with. That austerity is the whole appeal of the system (it's minimal and rigorously correct) and also why every definition is so verbose. The reason Rayo's number is famous isn't that it builds efficiently. It's that the real construction doesn't build at all: it uses self-reference. Something in the shape of "the smallest number no formula shorter than N can name." One clever, self-pointing formula gets you enormous power in a single move, instead of paying for every number along the way. And, as I'd find out, that move isn't even strictly available inside the system it's nominally playing in. More on that below.

Nobody had ever actually proven that works

This is where it got interesting. I went looking for a rigorous version of that self-referential trick: a proof, mechanized or otherwise, that it's actually well-defined and doesn't quietly collapse into the Berry paradox it's dancing right up next to. There isn't one. Not a formalization in any proof assistant, not even a fully worked informal proof anywhere in the literature. Rayo's own account of it, in his book, is a prose sketch: "relied on a second-order language to characterize a non-semantic substitute for the notion of being named." That's a description of a strategy, not a theorem.

So I built two competing rigorous versions of it, in parallel, using a fleet of Claude Code agents running unattended (some local, some genuinely cloud-isolated, one round dispatched from my phone while away from my laptop) against a Lean 4 formalization library called Foundation.

The safer route swaps "true" for "provable," relative to one fixed theory: ordinary Peano arithmetic. Provability, unlike truth, can be expressed inside the theory itself, which is exactly the escape hatch Gödel built for his own incompleteness proof. This one closed completely: well-defined, on paper and machine-checked; the actual naming machinery formalized as real object-language logic; and, after three separate rounds hitting the same category of Lean plumbing issue (a proof library that had the right lemma the whole time, just not tagged where the automatic tactics would find it), the literal theorem (this construction eventually beats every function ordinary arithmetic can prove always finishes) closed sorry-free, checked against nothing but the standard, unavoidable axioms.

The harder route was Rayo's actual construction, attempted directly. The honest result: it's consistent, and it does name a specific number, but only if you grant a background assumption about mathematical truth that the popular description never states. Evaluating "what formulas name" needs a truth predicate, and by Tarski's undefinability theorem, first-order set theory cannot supply one for itself. You need something close to Morse-Kelley set theory's strength to even make "true in the universe of sets" meaningful for the formulas involved. Grant that, and the number is real. Withhold it, and the construction names nothing at all. This is the payoff of the foreshadowing earlier: Rayo's trick is something of a hack, not strictly "allowed" in the system he's nominally pricing definitions in, even though everyone broadly knows what he means in a pragmatic way. I initially thought nobody had written this down before. Not quite: a later audit of the googology community's own technical literature found the point fully documented there from 2018 onward, with one wiki analysis naming Morse-Kelley exactly, though it remains invisible in every mainstream account. So: an independent rediscovery, and a real correction to how the thing gets talked about everywhere outside that community.

The part that ties it together

Once both were nailed down, the connection was almost too clean: they're the same naming machine, running on different fuel. The provability route tops out at a growth rate mathematicians call ε₀, a specific, well-understood ceiling. The truth route doesn't top out anywhere; it climbs past every fixed notation anyone has a name for. And the entire gap between those two outcomes traces to exactly one variable: how strong a notion of "true" you're willing to assume exists. Not a cleverer trick. Not a different mechanism. Just a sharper commitment, bought at a sharp, discrete jump rather than a smooth dial you can turn partway.

And the ladder doesn't stop there. The stronger metatheory Rayo's number needs is itself a formal language, so you can play the identical naming game over it, and by the same argument that game's winner eventually dominates Rayo's. To make that concrete: one level up, "the successor of Rayo's number" is a formula of a few thousand symbols, while by definition the same number costs more than a googol symbols in first-order set theory. A few thousand against 10^100. Crucially, none of this can happen inside first-order set theory itself: define "the biggest number nameable in n symbols" within the same system doing the naming and you get the Berry paradox, not a number. The bigger number always comes from stepping one level up, and the levels never run out. There is no top.

That's the actual answer to the question I started with. Growth doesn't scale with specification cost the way you'd hope for a tidy story. It scales with something closer to how much you're willing to assume about truth itself, and that's a genuinely strange thing to have gotten a mechanically checked, honest answer to, out of a rabbit hole that started with two YouTube videos.

The mess along the way was real too, and worth being honest about rather than tidying out of the story: a mis-cited source paper caught and fixed, an agent that quietly disabled commit signing when it hit friction (caught, reverted, never repeated after I told the next one explicitly not to), and more than one git collision from me editing the same working directory a background agent was still using. None of it changed the results. All of it is sitting in the commit history rather than smoothed over, which feels like the right way to have done it.

If you want to actually look at any of it, the whole thing (the Lean proofs, the paper arguments, the false starts) is public: github.com/EdwardAThomson/mathematics, under large-numbers/.