User:Azerty/Lambda Calculus Busy Beaver

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, (\1 1) (\\2 (1 2)) 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.

BBλ_db(n)	Value	Champion	Discovered By
7	7	\1 1 1 1 1 1
8	≥ 16	(\1 1) (\\2 (1 2))	Azerty & John Tromp & Bertram Felgenhauer
9	≥ 68	(\1 1) (\\2 (2 (1 2)))	John Tromp & Bertram Felgenhauer
10	$\ge 3\uparrow \uparrow 3+3>7.625\times 10^{12}$	(\1 1 1) (\\2 (2 (2 1)))
11	$\ge 3\uparrow \uparrow 4+3>10^{10^{12}}$	(\1 1 1 1) (\\2 (2 (2 1)))
12	$>10{\uparrow }^{3}16$	(\1 1 1) (\1 (\\2 (2 1)) 1)	mxdys and racheline
13	$>10{\uparrow }^{3}10{\uparrow }^{3}10{\uparrow }^{2}6$	(\1 1) (\1 (\1 (\\2 (2 1)) 2))	mxdys
14	$>10{\uparrow }^{3}10{\uparrow }^{3}10{\uparrow }^{3}16$	(\1 1 1 1 1) (\1 (\\2 (2 1)) 1)
15	$>f_{\omega +1}(2\uparrow \uparrow 6)$	(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))	Gustavo Melo
18	$>f_{{\omega }^{\omega }}(2\uparrow \uparrow 18)$	(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))	50_ft_lock
22	$>f_{{\omega }^{\omega +2}}(2)$	(\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))	Patcail
23	$>f_{{\zeta }_0}(15)$	(\1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))	Patcail
24	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}(12)$	(\1 1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))	Patcail
25	$>f_{\psi ({\mathrm{\Omega }}_{\omega })}(f_{{\omega }^{\omega +2}}(2))$	(\1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))	Patcail
26	$>f_{\psi ({\mathrm{\Omega }}_{\omega }+1)}(4)$	(\1 1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))	Patcail

Most champions are currently taken from binary BBλ.