'''Busy Beaver for lambda calculus''' ('''BBλ''') is a variation of the [[Busy Beaver]] problem for [https://en.wikipedia.org/wiki/Lambda_calculus lambda calculus] invented by John Tromp. BBλ(n) = the maximum normal form size of any closed lambda term of size n. Like the traditional Busy Beaver functions, it is uncomputable (and in fact grows faster than any computable function). If you are not familiar with lambda calculus and beta-reduction, it is recommended to start with that article.

Size is measured in bits using [https://tromp.github.io/cl/Binary_lambda_calculus.html Binary Lambda Calculus] which is a binary prefix-free encoding for all closed lambda calculus terms.

== Analogy to Turing machines ==
We evaluate terms by applying ''beta-reductions'' until they reach a ''normal form''. As an analogy to [[Turing machines]]:
* ''Lambda terms'' are like TM configurations (tape + state + position).
* Applying ''beta-reduction'' to a term is like taking a TM step.
* A term is in ''normal form'' if no beta-reductions can be applied. This is like saying the term has halted.
* A term may or may not be reducible to a normal form. If it is, this is like saying the term halts.
* Determining whether a term is reducible to a normal form is an undecidable problem equivalent to the halting problem.

Note: That unlike for Turing machines, evaluating lambda terms is non-deterministic. Specifically, there may be multiple beta-reductions possible in a given term. However, if a term can be reduced to a normal form, that normal form is unique. It is not possible to reduce the original term to any different normal form. A term is '''strongly normalizing''' if any choice of beta-reductions will lead to this normal form and '''weakly normalizing''' if there exist divergent reduction paths which never reach the normal form.

== Proof of Uncomputability ==
The proof that BBλ(n) is uncomputable is very similar to Radó's original proof that Σ(n) is uncomputable. Proof by contradiction:

Assume BBλ is computable and so there exists a term ''f'' which computes it on [[wikipedia:Church_encoding|Church numerals]]. In other words: for all <math>n \in \N</math>: <math>(f \; C_n)</math> beta reduces to normal form <math>C_{BB\lambda(n)}</math> (where <math>C_n</math> denotes the Church numeral ''n''). Denote the binary lambda encoded size of ''f'' as ''k''. Consider the term <math>f \; (C_2 \; C_n)</math> which has size <math>2+k+2+(5\times2+6)+(5n+6) = 5n + k + 26</math> bits. This term reduces to <math>C_{BB\lambda(n^2)}</math> which has size <math>5 \cdot BB\lambda(n^2) + 6</math> bits. But for sufficiently large n, <math>n^2 > 5n + k + 26</math> and so <math>5 \cdot BB\lambda(n^2) + 6 > BB\lambda(5n + k + 26)</math>. But this is a contradiction, we've found a <math>5n + k + 26</math> bit term which reduces to a normal form larger than <math>BB\lambda(5n + k + 26)</math>.

Thus BBλ(n) is uncomputable. A variation of this argument shows that BBλ(n) eventually dominates all computable functions.

== Binary Lambda Encoding ==
A lambda term using [https://en.wikipedia.org/wiki/De_Bruijn_indices De Bruijn indexes] is defined inductively as:
* Variables: For any <math>n \in \mathbb{Z}^+</math>, Var(''n'') is a term. It represents a variable bound by the lambda expression ''n'' above this one (the De Bruijn index). It is typically written simply as <code>n</code>.
* Lambdas: For any term ''T'', Lam(''T'') is a term. It represents a unary function with function body ''T''. It is typically written <math>\lambda T</math> or <code>\T</code>.
* Applications: For any terms ''T, U'', App(''T, U'') is a term. It represents applying function ''T'' to argument ''U''. It is typically written <code>(T U)</code>.

We can think of this as a tree where each variable is a leaf, a lambda is a node with one child and applications are nodes with 2 children. A term is '''closed''' if every variable is bound. In other words, for every Var(''n'') leaf node, there exists ''n'' Lam() nodes above it in the tree of the term.

Encoding (''blc()'') is defined recursively:
<math display="block">\begin{array}{l}
blc(Var(n)) & = & 1^n 0 \\
blc(Lam(T)) & = & 00 \; blc(T) \\
blc(App(T, U)) & = & 01 \; blc(T) \; blc(U) \\
\end{array}</math>

For example, the [https://en.wikipedia.org/wiki/Church_encoding#Church_numerals Church numeral] 2: <math>\lambda f x. (f \; (f \; x))</math> = <code>\\(2 (2 1))</code> = <code>Lam(Lam(App(Var(2), App(Var(2), Var(1))))</code> is encoded as <code>00 00 01 110 01 110 10</code> or simply <code>0000011100111010</code> (spaces are not part of the encoding, only used for demonstration purposes) and thus has size 16 bits.

== Text Encoding conventions ==
For human readability, a text encoding and set of conventions is used in this article. As described earlier we encode a lambda term as:
* Var(''n'') -> <code>n</code>
* Lam(''T'') -> <code>(\T)</code>
* App(''T, U'') -> <code>(T U)</code>

However, parentheses are also dropped in certain cases by convention:
* The outermost parentheses are dropped: <code>Lam(1)</code> -> <code>\1</code> and <code>App(1, 2)</code> -> <code>1 2</code>.
* Parentheses are dropped immediately inside a Lam: <code>Lam(Lam(1))</code> -> <code>\\1</code> and <code>Lam(App(1, 1))</code> -> <code>\1 1</code>.
* Parentheses are dropped in nested Apps using left associativity: <code>App(App(1, 2), 3)</code> -> <code>1 2 3</code>. (Note: parentheses are still required for <code>App(1, App(2, 3))</code> -> <code>1 (2 3)</code>).

This is the convention used in John Tromp's code and so is used here for consistency.

== Champions ==
There are no closed lambda terms of size 0, 1, 2, 3 or 5 and so BBλ(n) is not defined for those values. The smallest closed lambda term is <code>\1</code> which has size 4.

For the rest of n ≤ 20: BBλ(n) = n is trivial and can be achieved via picking any n bit term already in normal form. For example <code>\\...\1</code> and <code>\\...\2</code> with k lambdas has size 2k+2 and 2k+3 respectively (for k ≥ 1 and k ≥ 2 respectively).

{| class="wikitable"
|+
!n
!BBλ(n)
!Champion
!Normal form
!Discovered By
|-
|21 || = 22 || <math>\lambda(\lambda 1 1) (1 (\lambda 2))</math>
| <math>\lambda(1(\lambda 2))(1(\lambda 2))</math>|| John Tromp & Bertram Felgenhauer
|-
|22 || = 24 || <math>\lambda(\lambda 1 1 1) (1 1)</math>
| <math>\lambda(1 1) (1 1) (1 1)</math>|| John Tromp & Bertram Felgenhauer
|-
|23 || = 26 || <math>\lambda(\lambda 1 1) (1 (\lambda\lambda 2))</math>
| <math>\lambda(1 (\lambda\lambda 2)) (1 (\lambda\lambda 2))</math>|| John Tromp & Bertram Felgenhauer
|-
|24 || = 30 || <math>\lambda(\lambda 1 1 1) (1 (\lambda 1))</math>
| <math>\lambda(1 (\lambda 1)) (1 (\lambda 1)) (1 (\lambda 1))</math>|| John Tromp & Bertram Felgenhauer
|-
|25 || = 42 || <math>\lambda(\lambda 1 1) (\lambda 1 (2 1))</math>
| <math>\lambda 1 (\lambda 1 (2 1)) (1 (1 (\lambda 1 (2 1))))</math> || John Tromp & Bertram Felgenhauer
|-
|26 || = 52 || <math>(\lambda 1 1) (\lambda\lambda 2 (1 2))</math>
| <math>\lambda\lambda 2 (\lambda\lambda 2 (1 2)) (1 (2 (\lambda\lambda 2 (1 2))))</math> || John Tromp & Bertram Felgenhauer
|-
|27 || = 44 || <math>\lambda\lambda(\lambda 1 1) (\lambda 1 (2 1))</math>
| <math>\lambda\lambda 1 (\lambda 1 (2 1)) (1 (1 (\lambda 1 (2 1))))</math> || John Tromp & Bertram Felgenhauer
|-
|28 || = 58 || <math>\lambda(\lambda 1 1) (\lambda 1 (2 (\lambda 2))))</math>
| <math>\lambda 1 (\lambda\lambda 1 (3 (\lambda 2))) (1 (\lambda 2 (\lambda\lambda 1 (4 (\lambda 2)))))</math>|| John Tromp & Bertram Felgenhauer
|-
| 29 || = 223|| <math>\lambda(\lambda 1 1) (\lambda 1 (1 (2 1)))</math>
| <pre>
\B (B (1 B))
where:
B = (A (A (1 A)))
A = (1 (\lambda 1 (1 (2 1))))
</pre>||John Tromp & Bertram Felgenhauer
|-
|30
|= 160
|<math>(\lambda 1 1 1) (\lambda\lambda 2 (1 2))</math>
| <pre>
\lambda\lambda 2 B A (1 (2 B A))
where:
B = (\lambda\lambda 2 A (1 (2 A)))
A = (\lambda\lambda 2 (1 2))
</pre>
|John Tromp & Bertram Felgenhauer
|-
|31
|= 267
|<math>(\lambda 1 1) (\lambda\lambda 2 (2 (1 2)))</math>
| <pre>
\lambda\lambda 2 A (2 A (C (2 A)))
where:
C = (2 A (2 A (1 B (2 A))))
B = (\lambda 3 A (3 A (1 (3 A))))
A = (\lambda\lambda 2 (2 (1 2)))
</pre>
|John Tromp & Bertram Felgenhauer
|-
|32
|= 298
|<math>\lambda(\lambda 1 1) (\lambda 1 (1 (2 (\lambda 2))))</math>
|
|John Tromp & Bertram Felgenhauer
|-
|33
|= 1812
|<math>\lambda(\lambda 1 1) (\lambda 1 (1 (1 (2 1))))</math>
| <pre>
\C (C (C (1 C)))
where:
C = (B (B (B (1 B)))
B = (A (A (A (1 A)))
A = (1 (\lambda 1 (1 (1 (2 1)))))
</pre>
|John Tromp & Bertram Felgenhauer
|-
|34 || <math>= \ 5 \left(2^{2^{2^2}}\right) + 6 = 327\,686</math>
| <math>(\lambda 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
| <math>C(2^{2^{2^2}})</math>|| John Tromp & Bertram Felgenhauer
|-
|35 || <math>= 5 \left(3^{3^3}\right) + 6 > 3.8 \times 10^{13}</math>
| <math>(\lambda 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>C(3^{3^3})</math>|| John Tromp & Bertram Felgenhauer
|-
|36 || <math>= 5 \left(2^{2^{2^3}}\right) + 6 > 5.7 \times 10^{77}</math>
| <math>(\lambda 1 1) (\lambda 1 (1 (\lambda\lambda 2 (2 1))))</math>
| <math>C(2^{2^{2^3}})</math>|| John Tromp & Bertram Felgenhauer
|-
|37 || <math> = BB\lambda(35)+2</math>
| <math>\lambda(\lambda 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>\lambda x. C(3^{3^3})</math>||mxdys, tromp, dyuan, sligocki
|-
|38 || <math>\ge 5 \left(2^{2^{2^{2^2}}}\right) + 6 > 10^{10^4}</math>
| <math>(\lambda 1 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
| <math>C(2^{2^{2^{2^2}}})</math>|| John Tromp & Bertram Felgenhauer
|-
|39 || <math>\ge 5 \left(3^{3^{3^3}}\right) + 6 > 10^{10^{12}}</math>
| <math>(\lambda 1 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>C(3^{3^{3^3}})</math>|| John Tromp & Bertram Felgenhauer
|-
|40 || <math> > (2\uparrow\uparrow)^{15} 33 > 10 \uparrow\uparrow\uparrow 16</math>
| <math>(\lambda 1 1 1) (\lambda 1 (\lambda\lambda 2 (2 1)) 1)</math>
| <math>\lambda x.T(k)</math> where <math>T(0)=x,\;T(n+1)=T(n)\;C(2)\;T(n)</math> and <math>k > (2\uparrow\uparrow)^{15} 33</math>|| mxdys and racheline
|-
|41 || <math>\ge 5 \left(3^{3^{85}}\right) + 6 > 10^{10^{40}}</math>
| <math>(\lambda 1 (\lambda 1 1) 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>C(3^{3^{85}})</math>||mxdys
|-
|42 ||<math> \ge BB\lambda(40)+2</math>
|<math>\lambda(\lambda 1 1 1) (\lambda 1 (\lambda\lambda 2 (2 1)) 1)</math>
| ||
|-
|43 ||<math> > 2 \uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 2 \uparrow\uparrow 8</math>
|<math>(\lambda 1 1) (\lambda 1 (\lambda 1 (\lambda\lambda 2 (2 1)) 2))</math>
| <math>\lambda x.T(k)</math> where <math>T(0)=x,\;T(n+1)=T(n)\;(\lambda y.y\;C(2)\;T(n))</math> and <math>k > 2 \uparrow\uparrow\uparrow 2 \uparrow\uparrow\uparrow 2 \uparrow\uparrow 8</math>||mxdys
|-
|44 || <math> > 10 \uparrow\uparrow\uparrow 10 \uparrow\uparrow\uparrow 16</math>
| <math>(\lambda 1 1 1 1) (\lambda 1 (\lambda\lambda 2 (2 1)) 1)</math>
| <math>\lambda x.T(k)</math> where <math>T(0)=x,\;T(n+1)=T(n)\;C(2)\;T(n)</math> and <math>k > (2\uparrow\uparrow)^{(2\uparrow\uparrow)^{15} 33 - 1} 33</math>||
|-
|45 || <math> \ge BB\lambda(43)+2</math>
| <math>\lambda(\lambda 1 1) (\lambda 1 (\lambda 1 (\lambda\lambda 2 (2 1)) 2))</math>
| ||
|-
|46 || <math> \ge BB\lambda(44)+2</math>
| <math>\lambda(\lambda 1 1 1 1) (\lambda 1 (\lambda\lambda 2 (2 1)) 1)</math>
| ||
|-
|47 ||
|
| ||
|-
|48 || <math> > 10 \uparrow\uparrow\uparrow 10 \uparrow\uparrow\uparrow 10 \uparrow\uparrow\uparrow 16</math>
| <math>(\lambda 1 1 1 1 1) (\lambda 1 (\lambda\lambda 2 (2 1)) 1)</math>
| <math>\lambda x.T(k)</math> where <math>T(0)=x,\;T(n+1)=T(n)\;C(2)\;T(n)</math> and <math>k > (2\uparrow\uparrow)^{(2\uparrow\uparrow)^{(2\uparrow\uparrow)^{15} 33 - 1} 33 - 1} 33</math>||
|-
|49
|<math>> f_{\omega+1}\left(\frac{2 \uparrow\uparrow 6}{2}\right)</math>
<math>> \text{Graham's number}</math>
|<math>(\lambda 1 1) (\lambda 1 (1 (\lambda\lambda 1 2 (\lambda\lambda 2 (2 1)))))</math>
|<math>C(N) \text{ for } N \approx f_{\omega+1}\left(\frac{2 \uparrow\uparrow 6}{2}\right)</math>
|[https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam Gustavo Melo]
|-
|...
|
|
|
|
|-
|61
|<math>> f_{\omega^{2 \uparrow\uparrow 18-1}}\left(2\right)</math>
|<math>(\lambda 1 1 1) (\lambda 1 (1 (\lambda\lambda\lambda 1 3 2 (\lambda\lambda 2 (2 1)))))</math>
|<math>C(N) \text{ for } N \approx f_{\omega^{2 \uparrow\uparrow 18-1}}\left(2\right)</math>
|[https://tromp.github.io/blog/2026/01/28/largest-number-revised 50_ft_lock]
|-
|...
|
|
|
|
|-
|86
|<math>> f_{\omega^{\omega^{2}}}\left(2\right)</math>
|<math>(\lambda 1 (\lambda\lambda\lambda\lambda 1 4 4 4 3 2 1) 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
|
|Patcail
|-
|...
|
|
|
|
|-
|90
|<math>> f_{\zeta_0}\left(15\right)</math>
|<math>(\lambda 1 1 (\lambda\lambda\lambda\lambda 1 4 4 4 3 2 1) 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
|
|Patcail
|-
|...
|
|
|
|
|-
|94
|<math>> f_{\psi(\Omega_\omega)}\left(12\right)</math>
<math>> \text{TREE}(G64)</math>
|<math>(\lambda 1 1 1 (\lambda\lambda\lambda\lambda 1 4 4 4 3 2 1) 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
|
|Patcail
|-
|95
|<math>> f_{\psi(\Omega_\omega)}\left(23\right)</math>
|<math>(\lambda 1 1 (\lambda\lambda\lambda\lambda 1 4 4 4 3 2 1) 1 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
|
|Patcail
|-
|96
|<math>> f_{\psi(\Omega_\omega)}\left(f_{\omega^{\omega^{2}}}\left(2\right)\right)</math>
|<math>(\lambda 1 (\lambda 1 (\lambda\lambda\lambda\lambda 1 4 4 4 3 2 1) 1 1 1 1) 1) (\lambda\lambda 2 (2 1))</math>
|
|Patcail
|-
|
|
|
|
|
|-
|100
|<math>> f_{\psi(\Omega_\omega)+1}\left(4\right)</math>
|<math>(\lambda 1 1 (\lambda 1 (\lambda\lambda\lambda\lambda 1 4 4 4 3 2 1) 1 1 1 1) 1) (\lambda\lambda 2 (2 1))</math>
|
|Patcail
|-
|
|
|
|
|
|-
|331
| lim(BMS)
|<code>too large to show</code>
|
|[https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/bms.lam Patcail & John Tromp & 50_ft_lock]
|
|-
|1850
|> Loader's number
|<code>too large to show</code>
|
|[https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634 John Tromp]
|}

Where <math>C(n)</math> represents the Church numeral ''n'' (<math>\lambda f x. f^n(x)</math>) written as <code>\\2 (2 ... (2 1)...)</code> with ''n'' 2s in this text representation.

== Oracle Busy Beaver ==
While BBλ grows uncomputably fast, one can define functions that grow much faster.

Let's define a higher order busy beaver function BBλ1 by providing oracle access to BBλ.

This is done by enriching the set of terms and possible reduction steps considered in the BB definition.

A 1-closed term is a term in de Bruijn notation that is closed with 1 additional lambda in front. Any variable bound to that lambda is a free variable '''f''' in the term.

An oracle reduction step reduces '''f''' t, where t is a closed normal form of size s, to Church numeral BBλ(s).

Note that this is almost identical to the oracle steps in Barendregt and Klop's "Applications of infinitary lambda calculus", except that they require t itself to be a church numeral. Allowing arbitrary closed t makes oracle steps more widely applicable while aligning with BBλ's focus on term sizes.

Now let BBλ1 be the maximum beta/oracle normal form size of any 1-closed lambda term of size n, or 0 if no 1-closed term of size n exists. This appears as sequence [[oeis:A385712|A385712]] in the OEIS.

The following table shows values of BBλ1 up to 22 plus a lower bound for 28, with larger values expressed in terms of function <math>f(n) = 6 + 5 \times BB \lambda(n)</math>:
{| class="wikitable"
|+
!n
!champion
!BBλ1
|-
|1
|
|0
|-
|2
|<code>1</code>
|1
|-
|3
|
|0
|-
|4
|<code>\1</code>
|4
|-
|5
|<code>\2</code>
|5
|-
|6
|<code>\\1</code>
|6
|-
|7
|<code>\\2</code>
|7
|-
|8
|<code>1 (\1)</code>
|<math>f(4) = 26</math>
|-
|9
|<code>\\2</code>
|9
|-
|10
|<code>1 (\\1)</code>
|<math>f(6) = 36</math>
|-
|11
|<code>1 (\\2)</code>
|<math>f(7) = 41</math>
|-
|12
|<code>1 (1 (\1))</code>
|<math>f^{2}(4) = 266</math>
|-
|13
|<code>1 (\\2)</code>
|<math>f(9) = 51</math>
|-
|14
|<code>1 (1 (\\1))</code>
|<math>f^{2}(6) = f(36) = 25 \times 2^{2^{2^{3}}}+36 > 2.85 \times 10^{78}</math>
|-
|15
|<code>1 (1 (\\2))</code>
|<math>f^{2}(7) = f(41) \geq 25 \times 3^{3^{85}}+36 > 10^{10^{40}}</math>
|-
|16
|<code>1 (1 (1 (\1)))</code>
|<math>f^{3}(4) = f(266)</math>
|-
|17
|<code>1 (1 (\\\2))</code>
|<math>f^2(9) = f(51)</math>
|-
|18
|<code>1 (\1) 1 (\1)</code>
|<math>f^4(4) </math>
|-
|19
|<code>1 (1 (1 (\\2)))</code>
|<math>f^3(7)</math>
|-
|20
|<code>1 (\\1) 1 (\1)</code>
|<math>f^6(4)</math>
|-
|21
|<code>1 (\\2) 1 (\1)</code>
|<math>f^7(4)</math>
|-
|22
|<code>1 (1 (\1)) 1 (\1)</code>
|<math>f^{52}(4)</math>
|-
|...
|
|
|-
|28
|<code>1 (\1) 1 (\1) 1 (\1)</code>
|<math>\ge f^{BB \lambda(f^3(4))}(4)</math>
|}
We can generalize BBλ1 to BBλα for ordinals α by using oracle function BBλα-1 for successor ordinal a, and oracle function (\n -> BBλα[n](n)) for limit ordinal α, assuming well-defined fundamental sequences up to α. Because of limited oracle inputs, all oracle busy beavers have identical values up to n=11.

== De Bruijn ==
We can use De Bruijn index instead of binary to evaluate lambda calculus size. To get the size of an expression, convert it into De Bruijn index then count the number of lambdas / backslashes and numbers. By example, <code>(\1 1) (\\2 (1 2))</code> is size 8 because it has 3 backslashes and 5 numbers.

For n < 7, BBλ_db(n) = n is trivial and can be achieved via picking any size n term already in normal form, like BBλ(m) for m ≤ 20.
{| class="wikitable"
!BBλ_db(n)
!Value
!Champion
!Discovered By
|-
|7
|≥ 7
|<code>\1 1 1 1 1 1</code>
|
|-
|8
|≥ 16
|<code>(\1 1) (\\2 (1 2))</code>
|[[User:Azerty|Azerty]] & John Tromp & Bertram Felgenhauer
|-
|9
|≥ 68
|<code>(\1 1) (\\2 (2 (1 2)))</code>
|John Tromp & Bertram Felgenhauer
|-
|10
|<math>\ge 3 \uparrow\uparrow 3 + 3 > 7.625 \times 10^{12}</math>
|<code>(\1 1 1) (\\2 (2 (2 1)))</code>
|
|-
|11
|<math>\ge 3 \uparrow\uparrow 4 + 3 > 10^{10^{12}}</math>
|<code>(\1 1 1 1) (\\2 (2 (2 1)))</code>
|
|-
|12
|<math>> 10 {\uparrow}^{3} 16</math>
|<code>(\1 1 1) (\1 (\\2 (2 1)) 1)</code>
|mxdys and racheline
|-
|13
|<math>> 10 {\uparrow}^{3} 10 {\uparrow}^{3} 10 {\uparrow}^{2} 6</math>
|<code>(\1 1) (\1 (\1 (\\2 (2 1)) 2))</code>
|mxdys
|-
|14
|<math>> 10 {\uparrow}^{3} 10 {\uparrow}^{3} 10 {\uparrow}^{3} 16</math>
|<code>(\1 1 1 1 1) (\1 (\\2 (2 1)) 1)</code>
|
|-
|15
|<math>> f_{\omega+1}(2 \uparrow\uparrow 6)</math>
|<code>(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))</code>
|[https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam Gustavo Melo]
|-
|18
|<math>> f_{\omega^\omega}(2 \uparrow\uparrow 18)</math>
|<code>(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))</code>
|[https://tromp.github.io/blog/2026/01/28/largest-number-revised 50_ft_lock]
|-
|22
|<math>> f_{\omega^{\omega+2}}(2)</math>
|<code>(\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|23
|<math>> f_{\zeta_0}(15)</math>
|<code>(\1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|24
|<math>> f_{\psi(\Omega_\omega)}(12)</math>
|<code>(\1 1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|25
|<math>> f_{\psi(\Omega_\omega)}(f_{\omega^{\omega+2}}(2))</math>
|<code>(\1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
|Patcail
|-
|26
|<math>> f_{\psi(\Omega_\omega+1)}(4)</math>
|<code>(\1 1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
|Patcail
|}

== See Also ==

* https://oeis.org/A333479
* [https://tromp.github.io/blog/2023/11/24/largest-number The largest number representable in 64 bits]. 24 Nov 2023. John Tromp.
* [https://tromp.github.io/cl/Binary_lambda_calculus.html Binary Lambda Calculus]. John Tromp.
* https://github.com/tromp/AIT/tree/master/BB
[[category:Functions]]