BusyBeaverWiki - Recent changes [en]

Holdouts lists

Polygon — Tue, 12 May 2026 14:46:36 GMT

Downloadable Holdouts Lists: fixed table

← Older revision		Revision as of 14:46, 12 May 2026
(One intermediate revision by the same user not shown)
Line 29:		Line 29:
	!4-symbol		!4-symbol
	\|0		\|0
	\|12,~~049~~,~~358~~		\|11,362,197
	\|		\|
	\|		\|
Line 44:		Line 44:
	\|-		\|-
	!6-symbol		!6-symbol
	\|~~437~~,~~729~~		\|432,360
	\|		\|
	\|		\|

BB(2,6)

Polygon — Tue, 12 May 2026 14:39:40 GMT

Stage 4: added new reduction

← Older revision		Revision as of 14:39, 12 May 2026
Line 1,124:		Line 1,124:
	\|437,729		\|437,729
	\|0.32%		\|0.32%
			\|TODO
			\| ---
			\| ---
			\|TODO
			\|-
			\|437,729
			\|432,360
			\|1.23%
	\|TODO		\|TODO
	\| ---		\| ---

TMBR: May 2026

Tjligocki — Tue, 12 May 2026 00:23:31 GMT

Holdouts: Updated BB(2,7)

← Older revision		Revision as of 00:23, 12 May 2026
Line 22:		Line 22:
	**Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to '''501,914'''<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1501664852953792513][https://discord.com/channels/960643023006490684/1084047886494470185/1501812428113973268]</sup>, then to '''439,120''' again using the inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502436063103291492]</sup> In total this was a '''16.71%''' reduction.		**Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to '''501,914'''<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1501664852953792513][https://discord.com/channels/960643023006490684/1084047886494470185/1501812428113973268]</sup>, then to '''439,120''' again using the inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502436063103291492]</sup> In total this was a '''16.71%''' reduction.
	*[[BB(2,7)]]		*[[BB(2,7)]]
	** Terry Ligocki enumerated ~~30K~~ more subtasks, increasing the number of holdouts to '''~~775~~,~~799~~,~~715~~'''. A total of ~~250K~~ subtasks out of the 1 million subtasks (or '''25%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659]</sup>		** Terry Ligocki enumerated 50K more subtasks, increasing the number of holdouts to '''837,815,405'''. A total of 270K subtasks out of the 1 million subtasks (or '''27%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659]</sup>

	[[Category:This Month in Beaver Research\|2026-05]]		[[Category:This Month in Beaver Research\|2026-05]]

BB(2,7)

Tjligocki — Tue, 12 May 2026 00:22:12 GMT

Stage 1: Added 27xxxx and 28xxxx results

← Older revision		Revision as of 00:22, 12 May 2026
Line 34:		Line 34:
	\|-		\|-
	\|00-09xxxx		\|00-09xxxx
	\|rowspan='11'\|Terry Ligocki		\|rowspan='13'\|Terry Ligocki
	\|Yes		\|Yes
	\|309,868,865		\|309,868,865
	\|rowspan='11'\|[https://drive.google.com/drive/folders/11AiZYiKJq7v0ns9o5nt-xUsSgSpcuNvZ?usp=drive_link Google Drive]		\|rowspan='13'\|[https://drive.google.com/drive/folders/11AiZYiKJq7v0ns9o5nt-xUsSgSpcuNvZ?usp=drive_link Google Drive]
	\|-		\|-
	\|10-19xxxx		\|10-19xxxx
Line 72:		Line 72:
	\|-		\|-
	\|27xxxx		\|27xxxx
			\|Yes
			\|35,295,482
			\|-
			\|28xxxx
			\|Yes
			\|26,720,208
			\|-
			\|29xxxx
	\|No		\|No
	\|TBD		\|TBD
	\|-		\|-
	\|~~28xxxx~~		\|30xxxx
	\|No		\|No
	\|TBD		\|TBD
	\|-		\|-
	\|29-99xxxx		\|31-99xxxx
	\|TBD		\|TBD
	\|No		\|No
Line 88:		Line 96:
	\| ---		\| ---
	\| ---		\| ---
	\|'''~~775~~,~~799~~,~~715~~'''		\|'''837,815,405'''
	\| ---		\| ---
	\|-		\|-

BB(3,4)

XnoobSpeakable — Mon, 11 May 2026 19:06:39 GMT

Phase 3: fix sigfigs consistancy

← Older revision		Revision as of 19:06, 11 May 2026
(2 intermediate revisions by the same user not shown)
Line 494:		Line 494:

	Phase 3 began with Andrew Ducharme applying a FAR decider by mxdys. The following stages were done by XnoobSpeakable. The "Substages" column refers to the amount of separate runs of deciders being applied to the full holdout list, the files are not split into smaller chunks ("Subtasks") like in Phase 2. (Note that Phase 2 stage 9 did actually use substages, like all of Phase 3.)		Phase 3 began with Andrew Ducharme applying a FAR decider by mxdys. The following stages were done by XnoobSpeakable. The "Substages" column refers to the amount of separate runs of deciders being applied to the full holdout list, the files are not split into smaller chunks ("Subtasks") like in Phase 2. (Note that Phase 2 stage 9 did actually use substages, like all of Phase 3.)

	~~Stage 2 is currently in progress, with 2 substages completed. The amount of holdouts is unclear due to a minor discrepancy with the predicted and observed counts.~~

	{\| class="wikitable sortable" style="text-align: left"		{\| class="wikitable sortable" style="text-align: left"
Line 520:		Line 518:
	\|XnoobSpeakable		\|XnoobSpeakable
	\|12,049,358		\|12,049,358
	\|~~≤11~~,~~368~~,~~507~~		\|11,362,197
	\|		\|5.70%
	\|Phase 3 stage 2		\|Phase 3 stage 2
	\|3/4 ~~(in prog.)~~		\|4
	\|[https://drive.google.com/drive/folders/1lNKc_GF2sa5ZfosleAlMNBQ3uJV4qClo Google Drive]		\|[https://drive.google.com/drive/folders/1lNKc_GF2sa5ZfosleAlMNBQ3uJV4qClo Google Drive]
	\|No		\|No

SKI Calculus

Sligocki — Mon, 11 May 2026 01:42:18 GMT

link LC

← Older revision		Revision as of 01:42, 11 May 2026
Line 1:		Line 1:
	A '''SKI calculus''' program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.		A '''SKI calculus''' program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.

	Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.		Like [[Lambda Calculus\|lambda calculus]], SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.

	* <code>Ix -> I</code>		* <code>Ix -> I</code>

(Article title)

C7X — Sun, 10 May 2026 21:50:09 GMT

← Older revision		Revision as of 21:50, 10 May 2026
Line 1:		Line 1:
			{{delete\|Looks like things covered elsewhere on this wiki}}

	La funzione bb(n) e incalcolabile, anche se, gli stati fanno crescere velocemente, ma i simboli con gli stati ancora di piu!, quindi dobbiamo fare computer con piu potenza di calcolo e altre cose!		La funzione bb(n) e incalcolabile, anche se, gli stati fanno crescere velocemente, ma i simboli con gli stati ancora di piu!, quindi dobbiamo fare computer con piu potenza di calcolo e altre cose!

SKI Calculus

C7X — Sun, 10 May 2026 21:43:41 GMT

Replace with archived version

← Older revision		Revision as of 21:43, 10 May 2026
Line 183:		Line 183:

	== See Also ==		== See Also ==
			[https://web.archive.org/web/20250217071017/https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function] (archived)

	[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]		[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]

	[[Category:Functions]]		[[Category:Functions]]

SKI Calculus

JLM — Sun, 10 May 2026 15:58:48 GMT

Remove suspicious link to missing resource.

← Older revision		Revision as of 15:58, 10 May 2026
Line 183:		Line 183:

	== See Also ==		== See Also ==
	~~[https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function] (archived)~~

	[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]		[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]

	[[Category:Functions]]		[[Category:Functions]]

BB(2,6)

Polygon — Sun, 10 May 2026 12:58:53 GMT

Stage 4: added runtimes where available

← Older revision		Revision as of 12:58, 10 May 2026
Line 1,100:		Line 1,100:
	\|502,532		\|502,532
	\|4.68%		\|4.68%
	\|~~TODO~~		\|4.1
	\| ---		\| ---
	\| ---		\| ---
Line 1,116:		Line 1,116:
	\|439,120		\|439,120
	\|12.51%		\|12.51%
	\|~~TODO~~		\|42.87
	\| ---		\| ---
	\| ---		\| ---

Lambda Calculus

Tromp — Sun, 10 May 2026 10:38:27 GMT

Analogy to Turing machines

← Older revision		Revision as of 10:38, 10 May 2026
(3 intermediate revisions by the same user not shown)
Line 1:		Line 1:
	'''Lambda calculus''' is a model of computation developed by Alonzo Church (of Church-Turing thesis fame) in ~~1936~~. If you are not familiar with lambda calculus and beta-reduction, it is recommended to start with [[wikipedia:Lambda_calculus\|this article]].		'''Lambda calculus''' is a model of computation developed by Alonzo Church (of Church-Turing thesis fame) in 1932. If you are not familiar with lambda calculus and beta-reduction, it is recommended to start with [[wikipedia:Lambda_calculus\|this article]].

	'''BBλ''' is the [[Busy Beaver]] problem for lambda calculus, where BBλ(n) is the maximum normal form size of any closed lambda term of size n (or 0 if no closed term of size n exists). Size is measured in bits using [https://tromp.github.io/cl/Binary_lambda_calculus.html Binary Lambda Calculus], a binary prefix-free encoding for all closed lambda calculus terms. Pioneered by John Tromp, BBλ is uncomputable, and therefore grows faster than any computable function.		'''BBλ''' is the [[Busy Beaver]] problem for lambda calculus, where BBλ(n) is the maximum normal form size of any closed lambda term of size n (or 0 if no closed term of size n exists). Size is measured in bits using [https://tromp.github.io/cl/Binary_lambda_calculus.html Binary Lambda Calculus], a binary prefix-free encoding for all closed lambda calculus terms. Pioneered by John Tromp, BBλ is uncomputable, and therefore grows faster than any computable function.
Line 11:		Line 11:
	* Determining whether a term is reducible to a normal form is an undecidable problem equivalent to the halting problem.		* 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~~.		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 every beta-reduction sequence leads to this normal form and '''weakly normalizing''' if some sequence does (while others may diverge).

	== Proof of Uncomputability ==		== Proof of Uncomputability ==
Line 471:		Line 471:
	* [https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861 Binary Lambda Calculus]. John Tromp.		* [https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861 Binary Lambda Calculus]. John Tromp.
	* https://github.com/tromp/AIT/tree/master/BB		* https://github.com/tromp/AIT/tree/master/BB
			* https://github.com/ccz181078/BLC.git
	* https://docs.google.com/spreadsheets/d/1jZ6TK9m3xmXUlC69727T-8WwvhALcsp8FrK6DzgThtw		* https://docs.google.com/spreadsheets/d/1jZ6TK9m3xmXUlC69727T-8WwvhALcsp8FrK6DzgThtw
	[[category:Functions]]		[[category:Functions]]

BB(2,6)

Polygon — Sun, 10 May 2026 09:07:06 GMT

Stage 4: added new reduction

← Older revision		Revision as of 09:07, 10 May 2026
Line 1,120:		Line 1,120:
	\| ---		\| ---
	\|Inductive_inf.v --maxT 10000 --exploop		\|Inductive_inf.v --maxT 10000 --exploop
			\|-
			\|439,120
			\|437,729
			\|0.32%
			\|TODO
			\| ---
			\| ---
			\|TODO
	\|}		\|}

Holdouts lists

Polygon — Sun, 10 May 2026 08:48:35 GMT

Updated BB(4,3) and BB(2,6), added new BB(4,3) holdouts list

← Older revision		Revision as of 08:48, 10 May 2026
Line 22:		Line 22:
	\|0		\|0
	\|4		\|4
	\|5,~~641~~,~~006~~		\|5,127,263
	\|		\|
	\|		\|
Line 44:		Line 44:
	\|-		\|-
	!6-symbol		!6-symbol
	\|~~439~~,~~120~~		\|437,729
	\|		\|
	\|		\|
Line 62:		Line 62:
	!File		!File
	!Notes		!Notes
			\|-
			\|[[BB(4,3)]]
			\|[https://drive.google.com/drive/folders/1HBPZ17llVE_8wCy5FvRUFQ5MJsaYXAW- May 9th, 2026]
			\|@Andrew Ducharme
			\|5,127,263
			\|[https://drive.google.com/file/d/1xHukBgJnm1zctZkOMR0UzdQyzr4Fx5pC/view 4x3_holdouts_5127263.txt.zip]
			\|Work done by Andrew Ducharme
	\|-		\|-
	\|[[BB(3,4)]]		\|[[BB(3,4)]]

TMBR: May 2026

Polygon — Sun, 10 May 2026 08:44:19 GMT

Added BB(4,3) reduction

← Older revision		Revision as of 08:44, 10 May 2026
Line 16:		Line 16:

	== Holdouts ==		== Holdouts ==
			*[[BB(4,3)]]
			**Andrew Ducharme reduced the number of holdouts from 5,641,006 to '''5,127,263''', a '''9.11%''' reduction, with mxdys's new inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502750172407533628]</sup>
	*[[BB(2,6)]]		*[[BB(2,6)]]
	**Andrew Ducharme reduced the number of holdouts from 536,112 to '''527,232''' via Enumerate.py and TM-enum, a '''1.66%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1500218448951775383][https://discord.com/channels/960643023006490684/1084047886494470185/1501436678823477368 ~~<nowiki>[7]</nowiki>~~]</sup>		**Andrew Ducharme reduced the number of holdouts from 536,112 to '''527,232''' via Enumerate.py and TM-enum, a '''1.66%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1500218448951775383][https://discord.com/channels/960643023006490684/1084047886494470185/1501436678823477368]</sup>
	**Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to '''501,914'''<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1501664852953792513][https://discord.com/channels/960643023006490684/1084047886494470185/1501812428113973268]</sup>, then to '''439,120''' again using the inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502436063103291492]</sup> In total this was a '''16.71%''' reduction.		**Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to '''501,914'''<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1501664852953792513][https://discord.com/channels/960643023006490684/1084047886494470185/1501812428113973268]</sup>, then to '''439,120''' again using the inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502436063103291492]</sup> In total this was a '''16.71%''' reduction.
	*[[BB(2,7)]]		*[[BB(2,7)]]
	** Terry Ligocki enumerated 30K more subtasks, increasing the number of holdouts to '''775,799,715'''. A total of 250K subtasks out of the 1 million subtasks (or '''25%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 ~~<nowiki>[8]</nowiki>~~]</sup>		** Terry Ligocki enumerated 30K more subtasks, increasing the number of holdouts to '''775,799,715'''. A total of 250K subtasks out of the 1 million subtasks (or '''25%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659]</sup>

	[[Category:This Month in Beaver Research\|2026-05]]		[[Category:This Month in Beaver Research\|2026-05]]

1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF

DrDisentangle — Sun, 10 May 2026 08:30:42 GMT

Era structure: Era mass strictly increases

@@ Line 227: / Line 227: @@
    era  49  m=  33269  raw=   9522575  M([218, 572], 101, [1])
 </pre>
-The first 50 era boundaries with <code>|L| = 1</code>:
+=== Era mass strictly increases ===
-<pre>
+Define the nth era mass <math>\Phi_n</math> as the number of ones on the tape at the nth era boundary:
-  era      0  m=            0  raw=                  43  M([1], 4, [1])
+<math display="block">
-  era      1  m=            4  raw=                 120  M([1], 10, [1])
+\Phi_n = (a_1+a_2+a_3+\ldots) + c + 1,
-  era      7  m=          226  raw=                6843  M([25], 50, [1])
+</math>
-  era     12  m=         1212  raw=               69570  M([120], 41, [1])
+with <math>a_i</math> the runs of ones to the left of cursor, and <math>c</math> the run at the cursor. Then
-  era     18  m=         3656  raw=              315410  M([167], 116, [1])
+<math display="block">
-  era     27  m=         9453  raw=             1361310  M([329], 136, [1])
+\Phi_{n+1} \ge \Phi_n + 4.
-  era     43  m=        23055  raw=             5352785  M([675], 68, [1])
+</math>
-  era     50  m=        34317  raw=            10024293  M([642], 271, [1])
+In other words, <code>sum(L) + c</code> is strictly increasing across every single era boundary.
-  era     66  m=        65672  raw=            25849480  M([765], 528, [1])
+However, this does not prove the machine non-halting because it cannot be excluded at the moment that the halting path can be reached between era boundaries.
-  era     67  m=        67322  raw=            27097569  M([1139], 174, [1])
-  era     72  m=        76833  raw=            33882626  M([1278], 135, [1])
+The proof of mass increase was formalized in Lean. A human-readable writeup exists: [[File:Phi_strict.pdf]]. In short, for every non-halting rule the mass increase is shown to be <math>\ge 0</math>.
 == Current status (2026-04-29) ==

File:Phi strict.pdf

DrDisentangle — Sun, 10 May 2026 08:28:52 GMT

DrDisentangle uploaded File:Phi strict.pdf Text writeup of a Lean proof

New page

== Summary ==
Text writeup of a Lean proof

User:BadDisplayName

BadDisplayName — Sun, 10 May 2026 07:36:13 GMT

User account BadDisplayName was created

De Bruijn index

Azerty — Sun, 10 May 2026 06:30:19 GMT

← Older revision		Revision as of 06:30, 10 May 2026
(One intermediate revision by the same user not shown)
Line 3:		Line 3:
	Its attendant Busy Beaver problem is '''BBλ_db''' which uses De Bruijn index instead of binary to evaluate lambda calculus expression size. To calculate size, convert the lambda calculus expression into [[wikipedia:De_Bruijn_index\|De Bruijn index]], then count the number of backslashes (lambdas) and numbers. By example, <code>(\1 1) (\\2 (1 2))</code> is size 8 because it has 3 backslashes and 5 numbers.		Its attendant Busy Beaver problem is '''BBλ_db''' which uses De Bruijn index instead of binary to evaluate lambda calculus expression size. To calculate size, convert the lambda calculus expression into [[wikipedia:De_Bruijn_index\|De Bruijn index]], then count the number of backslashes (lambdas) 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.		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"		{\| class="wikitable"
	!BBλ_db(n)		!BBλ_db(n)
Line 26:		Line 26:
	\|-		\|-
	\|10		\|10
	\|		\|<math>\ge 3 \uparrow\uparrow 3 + 3 > 7.625 \times 10^{12}</math>
	\|<code>(\1 1 1) (\\2 (2 (2 1)))</code>		\|<code>(\1 1 1) (\\2 (2 (2 1)))</code>
	\|		\|
	\|-		\|-
	\|11		\|11
	\|		\|<math>\ge 3 \uparrow\uparrow 4 + 3 > 10^{10^{12}}</math>
	\|<code>(\1 1 1 1) (\\2 (2 (2 1)))</code>		\|<code>(\1 1 1 1) (\\2 (2 (2 1)))</code>
	\|		\|
	\|-		\|-
	\|12		\|12
	\|		\|<math>> 10 {\uparrow}^{3} 16</math>
	\|<code>(\1 1 1) (\1 (\\2 (2 1)) 1)</code>		\|<code>(\1 1 1) (\1 (\\2 (2 1)) 1)</code>
	\|mxdys and racheline		\|mxdys and racheline
	\|-		\|-
	\|13		\|13
	\|		\|<math>> 10 {\uparrow}^{3} 10 {\uparrow}^{3} 10 {\uparrow}^{2} 6</math>
	\|<code>(\1 1) (\1 (\1 (\\2 (2 1)) 2))</code>		\|<code>(\1 1) (\1 (\1 (\\2 (2 1)) 2))</code>
	\|mxdys		\|mxdys
	\|-		\|-
	\|14		\|14
	\|		\|<math>> f_{\omega}\left(f_{5}\left(2\right)\right)</math>
	\|<code>(\1 1 1) (\\1 (1 2) (\\2 (2 1)))</code>		\|<code>(\1 1 1) (\\1 (1 2) (\\2 (2 1)))</code>
	\|50_ft_lock		\|50_ft_lock
	\|-		\|-
	\|15		\|15
	\|		\|<math>> f_{\omega+1}(2 \uparrow\uparrow 6)</math>
	\|<code>(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))</code>		\|<code>(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))</code>
	\|Gustavo Melo		\|Gustavo Melo
	\|-		\|-
	\|18		\|18
	\|		\|<math>> f_{\omega^\omega}(2 \uparrow\uparrow 18)</math>
	\|<code>(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))</code>		\|<code>(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))</code>
	\|50_ft_lock		\|50_ft_lock
	\|-		\|-
	\|22		\|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>		\|<code>(\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
	\|Patcail		\|Patcail
	\|-		\|-
	\|23		\|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>		\|<code>(\1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
	\|Patcail		\|Patcail
	\|-		\|-
	\|24		\|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>		\|<code>(\1 1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
	\|Patcail		\|Patcail
	\|-		\|-
	\|25		\|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>		\|<code>(\1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
	\|Patcail		\|Patcail
	\|-		\|-
	\|26		\|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>		\|<code>(\1 1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
	\|Patcail		\|Patcail
	\|}		\|}

User:RobinCodes/Work on BB Domains

RobinCodes — Sun, 10 May 2026 06:02:19 GMT

Add BB(3,4) as active domain and add progress

← Older revision		Revision as of 06:02, 10 May 2026
(One intermediate revision by the same user not shown)
Line 2:		Line 2:
	As of May 2026,		As of May 2026,

	'''Domains with active filtering going on (decider-wise): [[BB(2,6)]], [[BB(7)]] - Andrew Ducharme'''		'''Domains with active filtering going on (decider-wise): [[BB(2,6)]], [[BB(7)]], [[BB(4,3)]] - Andrew Ducharme. [[BB(4,3)\|BB(3,4)]] - [[User:XnoobSpeakable\|XnoobSpeakable]]'''

	{\| class="wikitable"		{\| class="wikitable"
Line 43:		Line 43:

	[[BB(3,3)]]		[[BB(3,3)]]
	\| style="background: #A06B10;" \| 5,~~641~~,~~006~~		\| style="background: #A06B10;" \| 5,127,263
	No Handwork		No Handwork

Line 91:		Line 91:
	\|-		\|-
	! 6-symbol		! 6-symbol
	\| style="background: #A06B10;" \| ~~527~~,~~232~~		\| style="background: #A06B10;" \| 439,120
	No Handwork		No Handwork
	Andrew Ducharme,		Andrew Ducharme,

SKI Calculus

ADucharme — Sat, 09 May 2026 23:07:17 GMT

introduction reorganization

← Older revision		Revision as of 23:07, 9 May 2026
Line 1:		Line 1:
	~~Busy Beaver for SKI calculus (we will call it BB_SKI for now) is a variation of the [[Busy Beaver for lambda calculus\|Busy Beaver problem for lambda calculus]].~~		A '''SKI calculus''' program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.

	A SKI calculus program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.

	Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.		Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.
Line 9:		Line 7:
	* <code>Sxyz -> Sxz(yz)</code>		* <code>Sxyz -> Sxz(yz)</code>

	Note that <code>xyz</code> represent any valid trees, not just single combinators.		Note that <code>xyz</code> represent any valid trees, not just single combinators. We repeat this process and we say it terminates if the combinator cannot be beta-reduced.

	We repeat this process and we say it terminates if the combinator cannot be beta-reduced.

	BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.		Busy Beaver for SKI calculus ('''BB_SKI''') is a variation of the [[Busy Beaver for lambda calculus\|Busy Beaver problem for lambda calculus]]. BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.

	== Champions ==		== Champions ==

Busy Beaver for SKI calculus

ADucharme — Sat, 09 May 2026 23:04:50 GMT

ADucharme moved page Busy Beaver for SKI calculus to SKI Calculus standardization

New page

Busy Beaver for SKI calculus (we will call it BB_SKI for now) is a variation of the [[Busy Beaver for lambda calculus|Busy Beaver problem for lambda calculus]].

A SKI calculus program is a binary tree where the leaves are combinators, the three symbols <code>S</code>, <code>K</code>, <code>I</code>. Using parentheses to notate the tree, a simple example of a SKI program is <code>(((SK)S)((KI)S))</code>. We can omit parentheses by assuming they are left-binding by default, so we simplify our program to <code>SKS(KIS)</code>.

Like lambda calculus, SKI calculus has a process called beta-reduction. We change the tree according to any reducible redex.

* <code>Ix -> I</code>
* <code>Kxy -> Kx</code>
* <code>Sxyz -> Sxz(yz)</code>

Note that <code>xyz</code> represent any valid trees, not just single combinators.

We repeat this process and we say it terminates if the combinator cannot be beta-reduced.

BB_SKI(n) is defined as the size of the largest output of a terminating program of size n.

== Champions ==
{| class="wikitable"
! n !! Value !! Champion !! Discoverered by
|-
| 1 || = 1 || S || ?
|-
| 2 || = 2 || SS || ?
|-
| 3 || = 3 || SSS || ?
|-
| 4 || = 4 || SSSS || ?
|-
| 5 || = 6 || SSS(SS) || ?
|-
| 6 || ≥ 17 || SSS(SI)S || ?
|-
|7
|≥ 40
|S(SS)S(SS)S
|?
|-
|8
|≥ 41
|SII(S(S(SS)))S
|?
|-
|9
|≥ 79
|SII(SS(SSS))S
|?
|-
|10
|≥ 164
|SII(SS(SS(SS)))S
|?
|-
|11
|≥ 681
|SII(SS(SS(SSS)))S
|?
|-
|12
|≥ 1530
|SII(SS(SS(SS(SS))))S
|?
|-
|13
|≥ 65537
|S(S(SI))I(S(S(KS)K)I)KK
|?
|-
|14
|≥ 2^256+1
|S(S(S(SI)))I(S(S(KS)K)I)KK
|?
|-
|15
|> 2^2^2^2^21
|S(S(SSS)I)I(S(S(KS)K)I)KK
|?
|-
|16
|> 2^^19
|S(S(S(SSS))I)I(S(S(KS)K)I)KK
|?
|-
|17
|> 2^^2^128
|SSK(S(S(KS)K)I)(S(SI(SI))I)KK
|?
|-
|18
|> 2^^2^2^2^2^21
|SSK(S(S(KS)K)I)(S(S(SSS)I)I)KK
|?
|-
|19
|> 2^^^2^128
|S(SSK(S(SI(SI))I))I(S(S(KS)K)I)KK
|?
|-
|20
|> 2^^^2^2^2^2^21
|S(SSK(S(S(SSS)I)I))I(S(S(KS)K)I)KK
|?
|-
|21
|> 2^^^2^^19
|S(SSK(S(S(S(SSS))I)I))I(S(S(KS)K)I)KK
|?
|-
|25
|> Graham's Number
|SII(SI(SI(K(S(K(S(K(SS(K(K(S(S(KS)K)I)))))(SI)))K))))
| 2014MELO03
|}

== SK calculus ==
We can remove the <code>I</code> combinator and replace it by <code>(SKS)</code>, <code>(SKK)</code> or any <code>(SKx)</code>. These terms have a straightforward binary encoding where (prefix) application is 1, K=00, and S=01. Since n combinators take n-1 applications to combine, their code length is 2n + n-1 = 3n-1 bits.

=== Champions ===
{| class="wikitable"
! n !! bits !! Value !! Champion !! Discoverered by
|-
| 1 || 2 || = 1 || S || ?
|-
| 2 || 5 || = 2 || SS || ?
|-
| 3 || 8 || = 3 || SSS || ?
|-
| 4 || 11 || = 4 || SSSS || ?
|-
| 5 || 14 || = 6 || SSS(SS) || ?
|-
| 6 || 17 || ≥ 10 || SSS(SS)S || ?
|-
|7
| 20
|≥ 40
|S(SS)S(SS)S
|?
|-
|8
| 23
|≥ 41
|S(S(SS)S(SS)S)
|?
|-
|9
| 26
|≥ 42
|S(S(S(SS)S(SS)S))
|?
|-
|10
| 29
|≥ 66
|SS(SSS)(SS(SS))S
|?
|-
|11
| 32
|≥ 79
|SS(SSS)(SS(SSS))S
|?
|-
|12
| 35
|≥ 164
|SS(SKK)(SS)(SS(SS))S
|?
|-
|13
| 38
|≥ 681
|SS(SKK)(SS)(SS(SSS))S
|?
|-
|14
| 41
|≥ 1530
|SS(SKK)(SS)(SS(SS(SS)))S
|?
|-
|15
| 44
|≥ 7811
|SS(SKK)(SS)(SS(SS(SSS)))S
|?
|}

== See Also ==
[https://komiamiko.me/math/ordinals/2020/06/21/ski-numerals.html Lower bounds of this function] (archived)

[https://dallaylaen.github.io/ski-interpreter/ SKI interpreter]

[[Category:Functions]]

Lambda Calculus

ADucharme — Sat, 09 May 2026 23:02:00 GMT

See Also: add De Bruijn index, edit SKI calculus links

← Older revision		Revision as of 23:02, 9 May 2026
Line 465:		Line 465:

	== See Also ==		== See Also ==
	* [[Busy Beaver for SKI calculus]]		* [[Busy Beaver for SKI calculus\|SKI calculus]]
			* [[De Bruijn index]]
	* https://oeis.org/A333479		* https://oeis.org/A333479
	* [https://www.mdpi.com/1099-4300/28/5/494 The Largest Number Representable in 64 Bits]. 26 Apr 2026. John Tromp.		* [https://www.mdpi.com/1099-4300/28/5/494 The Largest Number Representable in 64 Bits]. 26 Apr 2026. John Tromp.

De Bruijn index

ADucharme — Sat, 09 May 2026 23:01:00 GMT

creation of page by taking section from lambda calculus page

New page

'''De Bruijn index''' is an alternative method to represent lambda calculus expressions.

Its attendant Busy Beaver problem is '''BBλ_db''' which uses De Bruijn index instead of binary to evaluate lambda calculus expression size. To calculate size, convert the lambda calculus expression into [[wikipedia:De_Bruijn_index|De Bruijn index]], then count the number of backslashes (lambdas) 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
|
|<code>(\1 1 1) (\\2 (2 (2 1)))</code>
|
|-
|11
|
|<code>(\1 1 1 1) (\\2 (2 (2 1)))</code>
|
|-
|12
|
|<code>(\1 1 1) (\1 (\\2 (2 1)) 1)</code>
|mxdys and racheline
|-
|13
|
|<code>(\1 1) (\1 (\1 (\\2 (2 1)) 2))</code>
|mxdys
|-
|14
|
|<code>(\1 1 1) (\\1 (1 2) (\\2 (2 1)))</code>
|50_ft_lock
|-
|15
|
|<code>(\1 1) (\1 (1 (\\1 2 (\\2 (2 1)))))</code>
|Gustavo Melo
|-
|18
|
|<code>(\1 1 1) (\1 (1 (\\\1 3 2 (\\2 (2 1)))))</code>
|50_ft_lock
|-
|22
|
|<code>(\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|23
|
|<code>(\1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|24
|
|<code>(\1 1 1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) (\\2 (2 1))</code>
|Patcail
|-
|25
|
|<code>(\1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
|Patcail
|-
|26
|
|<code>(\1 1 (\1 (\\\\1 4 4 4 3 2 1) 1 1 1 1) 1) (\\2 (2 1))</code>
|Patcail
|}

Lambda Calculus

ADucharme — Sat, 09 May 2026 22:49:45 GMT

removal of de bruijn index section, to be moved to new page

@@ Line 1: / Line 1: @@
-'''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 (or 0 if no closed term of size n exists). 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.
+'''Lambda calculus''' is a model of computation developed by Alonzo Church (of Church-Turing thesis fame) in 1936. If you are not familiar with lambda calculus and beta-reduction, it is recommended to start with [[wikipedia:Lambda_calculus|this 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.
+'''BBλ''' is the [[Busy Beaver]] problem for lambda calculus, where BBλ(n) is the maximum normal form size of any closed lambda term of size n (or 0 if no closed term of size n exists). Size is measured in bits using [https://tromp.github.io/cl/Binary_lambda_calculus.html Binary Lambda Calculus], a binary prefix-free encoding for all closed lambda calculus terms. Pioneered by John Tromp, BBλ is uncomputable, and therefore grows faster than any computable function.
 == Analogy to Turing machines ==
@@ Line 463: / Line 463: @@
 |}
 We can generalize BBλ<sub>1</sub> to BBλ<sub>α</sub> for ordinals α by using oracle function BBλ<sub>α-1</sub> for successor ordinal a, and oracle function (\n -> BBλ<sub>α[n]</sub>(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.
 == See Also ==
 * [[Busy Beaver for SKI calculus]]
 * https://oeis.org/A333479

Lambda Calculus

ADucharme — Sat, 09 May 2026 22:31:42 GMT

ADucharme deleted redirect Lambda Calculus by overwriting Deleted to make way for move from "Busy Beaver for lambda calculus"

Busy Beaver for lambda calculus

ADucharme — Sat, 09 May 2026 22:31:42 GMT

ADucharme moved page Busy Beaver for lambda calculus to Lambda Calculus over redirect standardization pf titles

New page

'''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 (or 0 if no closed term of size n exists). 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) = 0 for those values.
<math>C(n)</math> denotes Church numeral ''n'' = <math>\lambda f\lambda x. f^n(x)</math>.
In the last column, JT and BF abbreviate John Tromp and Bertram Felgenhauer. The [https://discord.com/channels/960643023006490684/1355653587824283678/1493455967868817429 smallest Cryptid known] currently is in 74 bits.

{| class="wikitable"
|+
!n
!BBλ(n)
!Champion
!Normal form
!Discovered By
|-
|4 || = 4 || <math>\lambda 1</math>
||| JT & BF
|-
|6 || = 6 || <math>\lambda\lambda 1</math>
||| JT & BF
|-
|7 || = 7 || <math>\lambda\lambda 2</math>
||| JT & BF
|-
|8 || = 8 || <math>\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|9 || = 9 || <math>\lambda\lambda\lambda 2</math>
||| JT & BF
|-
|10 || = 10 || <math>\lambda\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|11 || = 11 || <math>\lambda\lambda\lambda\lambda 2</math>
||| JT & BF
|-
|12 || = 12 || <math>\lambda\lambda\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|13 || = 13 || <math>\lambda\lambda\lambda\lambda\lambda 2</math>
||| JT & BF
|-
|14 || = 14 || <math>\lambda\lambda\lambda\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|15 || = 15 || <math>\lambda\lambda\lambda\lambda\lambda\lambda 2</math>
||| JT & BF
|-
|16 || = 16 || <math>\lambda\lambda\lambda\lambda\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|17 || = 17 || <math>\lambda\lambda\lambda\lambda\lambda\lambda\lambda 2</math>
||| JT & BF
|-
|18 || = 18 || <math>\lambda\lambda\lambda\lambda\lambda\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|19 || = 19 || <math>\lambda\lambda\lambda\lambda\lambda\lambda\lambda\lambda 2</math>
||| JT & BF
|-
|20 || = 20 || <math>\lambda\lambda\lambda\lambda\lambda\lambda\lambda\lambda\lambda 1</math>
||| JT & BF
|-
|21 || = 22 || <math>\lambda(\lambda 1 1) (1 (\lambda 2))</math>
| <math>\lambda(1(\lambda 2))(1(\lambda 2))</math>|| JT & BF
|-
|22 || = 24 || <math>\lambda(\lambda 1 1 1) (1 1)</math>
| <math>\lambda(1 1) (1 1) (1 1)</math>|| JT & BF
|-
|23 || = 26 || <math>\lambda(\lambda 1 1) (1 (\lambda\lambda 2))</math>
| <math>\lambda(1 (\lambda\lambda 2)) (1 (\lambda\lambda 2))</math>|| JT & BF
|-
|24 || = 30 || <math>\lambda(\lambda 1 1 1) (1 (\lambda 1))</math>
| <math>\lambda(1 (\lambda 1)) (1 (\lambda 1)) (1 (\lambda 1))</math>|| JT & BF
|-
|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>|| JT & BF
|-
|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>|| JT & BF
|-
|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>|| JT & BF
|-
|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>|| JT & BF
|-
| 29 || = 223|| <math>\lambda(\lambda 1 1) (\lambda 1 (1 (2 1)))</math>
| <math>\lambda B (B (1 B)) \text{ where}</math>
<math>B = (A (A (1 A)))</math>,
<math>A = (1 (\lambda 1 (1 (2 1))))</math>
||JT & BF
|-
|30
|= 160
|<math>(\lambda 1 1 1) (\lambda\lambda 2 (1 2))</math>
|
<math>\lambda\lambda 2 B A (1 (2 B A)) \text{ where}</math>
<math>B = (\lambda\lambda 2 A (1 (2 A)))</math>,
<math>A = (\lambda\lambda 2 (1 2))</math>
|JT & BF
|-
|31
|= 267
|<math>(\lambda 1 1) (\lambda\lambda 2 (2 (1 2)))</math>
|
<math>\lambda\lambda 2 A (2 A (C (2 A))) \text{ where}</math>
<math>C = (2 A (2 A (1 B (2 A))))</math>,
<math>B = (\lambda 3 A (3 A (1 (3 A))))</math>,
<math>A = (\lambda\lambda 2 (2 (1 2)))</math>
|JT & BF
|-
|32
|= 298
|<math>\lambda(\lambda 1 1) (\lambda 1 (1 (2 (\lambda 2))))</math>
|
|JT & BF
|-
|33
|= 1812
|<math>\lambda(\lambda 1 1) (\lambda 1 (1 (1 (2 1))))</math>
|
<math>\lambda C (C (C (1 C))) \text{ where}</math>
<math>C = (B (B (B (1 B)))</math>,
<math>B = (A (A (A (1 A)))</math>,
<math>A = (1 (\lambda 1 (1 (1 (2 1)))))</math>
|JT & BF
|-
|34 || <math>= 327\,686</math>
| <math>(\lambda 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
| <math>C(2^{2^{2^2}})</math>|| JT & BF
|-
|35 || <math>= 5 \cdot 3^{3^3} + 6</math>
<math> > 3.8 \times 10^{13}</math>
| <math>(\lambda 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>C(3^{3^3})</math>|| JT & BF
|-
|36 || <math>= 5 \cdot 2^{2^{2^3}} + 6</math>
<math> > 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>|| JT & BF
|-
|37 || <math> = 2 + BB\lambda(35)</math>
| <math>\lambda(\lambda 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>\lambda x. C(3^{3^3})</math>||mxdys & JT & dyuan & sligocki
|-
|38 || <math>= 5\cdot{2^{2^{2^{2^2}}}} + 6</math>
| <math>(\lambda 1 1 1 1 1) (\lambda\lambda 2 (2 1))</math>
| <math>C(2^{2^{2^{2^2}}})</math>|| JT & BF & CppDS & mxdys & sligocki & dyuan & charles
|-
|39 || <math>\ge 10^{10^{12}}</math>
| <math>(\lambda 1 1 1 1) (\lambda\lambda 2 (2 (2 1)))</math>
| <math>C(3^{3^{3^3}})</math>|| JT & BF
|-
|40 || <math> > 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)\text{ where}</math>
<math>T(0)=x</math>,
<math>T(n+1)=T(n)\;C(2)\;T(n)</math>,
<math>k > (2\uparrow\uparrow)^{15} 33</math>
|| mxdys & racheline
|-
|41 || <math>\ge 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 2 + BB\lambda(40)</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)\text{ where}</math>
<math>T(0)=x</math>,
<math>T(n+1)=T(n)\;(\lambda y.y\;C(2)\;T(n))</math>,
<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)\text{ where}</math>
<math>T(0)=x</math>,
<math>T(n+1)=T(n)\;C(2)\;T(n)</math>,
<math>k > (2\uparrow\uparrow)^{(2\uparrow\uparrow)^{15} 33 - 1} 33</math>||
|-
|45 || <math> \ge 2 + BB\lambda(43)</math>
| <math>\lambda(\lambda 1 1) (\lambda 1 (\lambda 1 (\lambda\lambda 2 (2 1)) 2))</math>
| ||
|-
|46 || <math> \ge 2 + BB\lambda(44)</math>
| <math>\lambda(\lambda 1 1 1 1) (\lambda 1 (\lambda\lambda 2 (2 1)) 1)</math>
| ||
|-
|47 || <math>> f_{\omega}\left(f_{5}\left(2\right)\right)</math>
| <math>(\lambda 1 1 1)(\lambda\lambda 1 (1 2) (\lambda\lambda 2 (2 1)))</math>
| ||50_ft_lock
|-
|48 || <math> > 10 \uparrow\uparrow\uparrow\uparrow 4</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> > Graham's number
|<math>(\lambda 1 1) (\lambda 1 (1 (\lambda\lambda 1 2 (\lambda\lambda 2 (2 1)))))</math>
|<math>C(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(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>
|
|[https://docs.google.com/document/d/1xlzaEQGarqnCocf4R2UWfqE3ck8YF_P32CmYxGXLhAI/edit?tab=t.0 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>
|
|[https://docs.google.com/document/d/1xlzaEQGarqnCocf4R2UWfqE3ck8YF_P32CmYxGXLhAI/edit?tab=t.0 Patcail]
|-
|...
|
|
|
|
|-
|94
|<math>> f_{\psi(\Omega_\omega)}\left(12\right)</math> > TREE(G64)
|<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>
|
|[https://docs.google.com/document/d/1xlzaEQGarqnCocf4R2UWfqE3ck8YF_P32CmYxGXLhAI/edit?tab=t.0 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>
|
|[https://docs.google.com/document/d/1xlzaEQGarqnCocf4R2UWfqE3ck8YF_P32CmYxGXLhAI/edit?tab=t.0 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>
|
|[https://docs.google.com/document/d/1xlzaEQGarqnCocf4R2UWfqE3ck8YF_P32CmYxGXLhAI/edit?tab=t.0 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>
|
|[https://docs.google.com/document/d/1xlzaEQGarqnCocf4R2UWfqE3ck8YF_P32CmYxGXLhAI/edit?tab=t.0 Patcail]
|-||||||-
|201
| > q(5)
|too large to show
|
|[https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/laver.lam JT & BF & 50_ft_lock]
|-||||||-
|331
| lim(BMS)
|too large to show
|
|[https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/bms.lam Patcail & JT & 50_ft_lock]
|-||||||-
|1850
|> Loader's number
|too large to show
|
|[https://codegolf.stackexchange.com/questions/176966/golf-a-number-bigger-than-loaders-number/274634#274634 JT]
|}

== 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
|<math>1</math>
|1
|-
|3
|
|0
|-
|4
|<math>\lambda 1</math>
|4
|-
|5
|<math>\lambda 2</math>
|5
|-
|6
|<math>\lambda \lambda 1</math>
|6
|-
|7
|<math>\lambda \lambda 2</math>
|7
|-
|8
|<math>1 (\lambda 1)</math>
|<math>f(4) = 26</math>
|-
|9
|<math>\lambda \lambda 2</math>
|9
|-
|10
|<math>1 (\lambda \lambda 1)</math>
|<math>f(6) = 36</math>
|-
|11
|<math>1 (\lambda \lambda 2)</math>
|<math>f(7) = 41</math>
|-
|12
|<math>1 (1 (\lambda 1))</math>
|<math>f^{2}(4) = 266</math>
|-
|13
|<math>1 (\lambda \lambda 2)</math>
|<math>f(9) = 51</math>
|-
|14
|<math>1 (1 (\lambda \lambda 1))</math>
|<math>f^{2}(6) = f(36) = 25 \times 2^{2^{2^{3}}}+36 > 2.85 \times 10^{78}</math>
|-
|15
|<math>1 (1 (\lambda \lambda 2))</math>
|<math>f^{2}(7) = f(41) \geq 25 \times 3^{3^{85}}+36 > 10^{10^{40}}</math>
|-
|16
|<math>1 (1 (1 (\lambda 1)))</math>
|<math>f^{3}(4) = f(266)</math>
|-
|17
|<math>1 (1 (\lambda \lambda \lambda 2))</math>
|<math>f^2(9) = f(51)</math>
|-
|18
|<math>1 (\lambda 1) 1 (\lambda 1)</math>
|<math>f^4(4) </math>
|-
|19
|<math>1 (1 (1 (\lambda \lambda 2)))</math>
|<math>f^3(7)</math>
|-
|20
|<math>1 (\lambda \lambda 1) 1 (\lambda 1)</math>
|<math>f^6(4)</math>
|-
|21
|<math>1 (\lambda \lambda 2) 1 (\lambda 1)</math>
|<math>f^7(4)</math>
|-
|22
|<math>1 (1 (\lambda 1)) 1 (\lambda 1)</math>
|<math>f^{52}(4)</math>
|-
|...
|
|
|-
|28
|<math>1 (\lambda 1) 1 (\lambda 1) 1 (\lambda 1)</math>
|<math>\ge f^{BB \lambda(f^3(4))}(4)</math>
|-
|29
|<math>1(\lambda 1)(\lambda 1 2 1)(\lambda 1)</math>
|<math>\ge f^{BB \lambda(f^{BB \lambda(f^4(4))+4}(4))+BB \lambda(f^4(4))+5}(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>> f_{\omega}\left(f_{5}\left(2\right)\right)</math>
|<code>(\1 1 1) (\\1 (1 2) (\\2 (2 1)))</code>
|50_ft_lock
|-
|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 ==

* [[Busy Beaver for SKI calculus]]
* https://oeis.org/A333479
* [https://www.mdpi.com/1099-4300/28/5/494 The Largest Number Representable in 64 Bits]. 26 Apr 2026. John Tromp.
* [https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861 Binary Lambda Calculus]. John Tromp.
* https://github.com/tromp/AIT/tree/master/BB
* https://docs.google.com/spreadsheets/d/1jZ6TK9m3xmXUlC69727T-8WwvhALcsp8FrK6DzgThtw
[[category:Functions]]

BB(4,3)

ADucharme — Sat, 09 May 2026 19:59:23 GMT

Stage 3: new inductive decider row

← Older revision		Revision as of 19:59, 9 May 2026
Line 596:		Line 596:
	\|		\|
	\| style="text-align:left" \|Enumerate.py -r --no-steps --exp-linear-rules --max-loops=100_000 --block-mult=3 --time=0.5 --lin-steps=0 --no-ctl		\| style="text-align:left" \|Enumerate.py -r --no-steps --exp-linear-rules --max-loops=100_000 --block-mult=3 --time=0.5 --lin-steps=0 --no-ctl
	\| rowspan="28" style="text-align:left" \|[https://drive.google.com/drive/folders/11FYe0CVDPczcgt4put3vsdGbeMWkM1S1?usp=sharing Google Drive]		\| rowspan="29" style="text-align:left" \|[https://drive.google.com/drive/folders/11FYe0CVDPczcgt4put3vsdGbeMWkM1S1?usp=sharing Google Drive]
	\|-		\|-
	\| style="text-align:left" \|Andrew Ducharme		\| style="text-align:left" \|Andrew Ducharme
Line 716:		Line 716:
	\|		\|
	\|Enumerate.py -r --no-steps --exp-linear-rules --max-loops=10_000_000 --block-mult=3 --time=10 --tape-limit=5000 --max-steps-per-macro=1_000_000 --lin-steps=0 --no-ctl		\|Enumerate.py -r --no-steps --exp-linear-rules --max-loops=10_000_000 --block-mult=3 --time=10 --tape-limit=5000 --max-steps-per-macro=1_000_000 --lin-steps=0 --no-ctl
			\|-
			\|Andrew Ducharme
			\|5,641,006
			\|5,127,263
			\|9.11%
			\|94.3
			\|
			\|
			\|Inductive decider maxT 1000 --exploop
	\|-		\|-
	\| style="text-align:center" \|'''Cumulative'''		\| style="text-align:center" \|'''Cumulative'''
	\|'''9,401,447'''		\|'''9,401,447'''
	\|'''5,~~641~~,~~006~~'''		\|'''5,127,263'''
	\|'''40.00%'''		\|'''45.46%'''
	\| ---		\| ---
	\| ---		\| ---

BB(2,6)

Polygon — Sat, 09 May 2026 11:05:10 GMT

Stage 4: attempted to reconstruct inductive decider commands

← Older revision		Revision as of 11:05, 9 May 2026
Line 1,103:		Line 1,103:
	\| ---		\| ---
	\| ---		\| ---
	\|~~TODO~~		\|Inductive_inf.v --maxT 1000 --arithseq --exploop
	\|-		\|-
	\|502,532		\|502,532
Line 1,119:		Line 1,119:
	\| ---		\| ---
	\| ---		\| ---
	\|~~TODO~~		\|Inductive_inf.v --maxT 10000 --exploop
	\|}		\|}

TMBR: May 2026

Polygon — Sat, 09 May 2026 10:05:52 GMT

Holdouts: Added new BB(6) reductions

← Older revision		Revision as of 10:05, 9 May 2026
(2 intermediate revisions by the same user not shown)
Line 10:		Line 10:
	** Size 49, by aparker, star and Shawn on 3 May (simulating [[wikipedia:Brocard's_problem\|Brocard's problem]]).<sup>[https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/brocard.mgrf]</sup>		** Size 49, by aparker, star and Shawn on 3 May (simulating [[wikipedia:Brocard's_problem\|Brocard's problem]]).<sup>[https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/brocard.mgrf]</sup>
	* The first non-trivial divergent GRF was found (size 15). It halts iff there exists some n ≥ 1 such that n+3 divides <math>Tetr(n) = \frac{n(n+1)(n+2)}{6}</math>.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500584497542987776]</sup> aparker<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500587569514283098]</sup> and star<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500595210919346337]</sup> proved that there is no such n.		* The first non-trivial divergent GRF was found (size 15). It halts iff there exists some n ≥ 1 such that n+3 divides <math>Tetr(n) = \frac{n(n+1)(n+2)}{6}</math>.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500584497542987776]</sup> aparker<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500587569514283098]</sup> and star<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1500595210919346337]</sup> proved that there is no such n.

			== Misc ==

			* mxdys made [https://github.com/ccz181078/busycoq/blob/BB6/verify/Inductive_inf.v his inductive decider] for [[History linear\|history-linear]] machines compilable into an executable file.<sup>[https://discord.com/channels/960643023006490684/960655108578881597/1501260508051800318]</sup>

	== Holdouts ==		== Holdouts ==
Line 15:		Line 19:
	*[[BB(2,6)]]		*[[BB(2,6)]]
	**Andrew Ducharme reduced the number of holdouts from 536,112 to '''527,232''' via Enumerate.py and TM-enum, a '''1.66%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1500218448951775383][https://discord.com/channels/960643023006490684/1084047886494470185/1501436678823477368 <nowiki>[7]</nowiki>]</sup>		**Andrew Ducharme reduced the number of holdouts from 536,112 to '''527,232''' via Enumerate.py and TM-enum, a '''1.66%''' reduction.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1500218448951775383][https://discord.com/channels/960643023006490684/1084047886494470185/1501436678823477368 <nowiki>[7]</nowiki>]</sup>
			**Using the new inductive decider by mxdys and TM-enum, Andrew Ducharme first reduced the number of holdouts from 527,232 to '''501,914'''<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1501664852953792513][https://discord.com/channels/960643023006490684/1084047886494470185/1501812428113973268]</sup>, then to '''439,120''' again using the inductive decider.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1502436063103291492]</sup> In total this was a '''16.71%''' reduction.
	*[[BB(2,7)]]		*[[BB(2,7)]]
	** Terry Ligocki enumerated ~~20K~~ more subtasks, increasing the number of holdouts to '''~~749~~,~~156~~,~~843~~'''. A total of ~~24K~~ subtasks out of the 1 million subtasks (or '''24%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[8]</nowiki>]</sup>		** Terry Ligocki enumerated 30K more subtasks, increasing the number of holdouts to '''775,799,715'''. A total of 250K subtasks out of the 1 million subtasks (or '''25%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 <nowiki>[8]</nowiki>]</sup>

	[[Category:This Month in Beaver Research\|2026-05]]		[[Category:This Month in Beaver Research\|2026-05]]

Holdouts lists

Polygon — Sat, 09 May 2026 09:45:40 GMT

Updated BB(2,6) holdout count

← Older revision		Revision as of 09:45, 9 May 2026
Line 44:		Line 44:
	\|-		\|-
	!6-symbol		!6-symbol
	\|~~501~~,~~914~~		\|439,120
	\|		\|
	\|		\|

BB(2,6)

Polygon — Sat, 09 May 2026 09:44:32 GMT

Stage 4: added new 12.51% reduction

← Older revision		Revision as of 09:44, 9 May 2026
Line 1,108:		Line 1,108:
	\|501,914		\|501,914
	\|0.12%		\|0.12%
			\|TODO
			\| ---
			\| ---
			\|TODO
			\|-
			\|501,914
			\|439,120
			\|12.51%
	\|TODO		\|TODO
	\| ---		\| ---

Sequences

Int-y1 — Sat, 09 May 2026 03:37:40 GMT

add fractran

← Older revision		Revision as of 03:37, 9 May 2026
Line 134:		Line 134:
	\|see [[Busy Beaver for lambda calculus#Champions]]		\|see [[Busy Beaver for lambda calculus#Champions]]
	\|[[oeis:A333479\|A333479]]		\|[[oeis:A333479\|A333479]]
			\|-
			\|[[Fractran]]
			\|BBf(n)
			\|The maximal number of steps that a Fractran program of size n can make on the integer 2 before eventually halting.
			\|see [[Fractran#Champions]]
			\|[[oeis:A395424\|A395424]]
	\|-		\|-
	\|}		\|}

Antihydra

MrSolis — Sat, 09 May 2026 01:41:12 GMT

← Older revision		Revision as of 01:41, 9 May 2026
(2 intermediate revisions by the same user not shown)
Line 97:		Line 97:

	== More Analysis ==		== More Analysis ==
	The <math>A</math> recurrence is equivalent to <math display="inline">D(0)=7, D(n+1)=\lceil D(n)\frac32\rceil</math><ref>Formalized proof at https://github.com/rwst/Antihydra-Basics/blob/main/AntihydraBasics/Antihydra.lean</ref><ref>Formalized proof at https://github.com/rwst/Antihydra-Basics/blob/main/AntihydraBasics/Basics.lean</ref>, by <math>H(n)=D(n)+1</math>, which is of advantage because in the Odlyzko-Wilf paper<ref>https://scholar.archive.org/work/usw755p7rzgtbnfpmkliokwdfa/access/wayback/https://www.cambridge.org/core/services/aop-cambridge-core/content/view/13435C4851F0CA24F64E08357C9D64F1/S0017089500008272a.pdf/div-class-title-functional-iteration-and-the-josephus-problem-div.pdf</ref> they showed that <math display="inline">D(n)=\lfloor K\cdot(\frac32)^n\rfloor</math>, for some <math>K</math>. They showed this for starting value <math>D(0)=1</math> but the proof works perfectly for any starting value except that the constant <math>K</math> will be different<ref>Formalized proof at https://github.com/rwst/Antihydra-Basics/blob/main/AntihydraBasics/Constant.lean</ref>. This means that the halting problem is a question of the parities of <math>D(n)</math> (as hinted above). However, a similar question on the parity of <math display="inline">\lfloor \xi\cdot(\frac32)^n\rfloor</math> has come up with [https://en.wikipedia.org/wiki/Mahler%27s_3/2_problem Mahler's Z-number problem]. That problem is formulated as a condition on the fractional parts of <math display="inline">\xi\cdot(\frac32)^n</math> but this is just another form. The Z-number problem is a long-standing open question and it could be answered if it were proven that <math display="inline">\{ \xi\cdot(\frac32)^n\}</math>, with <math>\{x\}</math> the fractional part of <math>x</math>, is uniformly distributed (or equidistributed) over <math>(0,1(</math>. A positive answer to that could also mean that the parity vector of <math>D(n)</math> is normal and thus a random walk.		The <math>A</math> recurrence is equivalent to <math display="inline">D(0)=7, D(n+1)=\lceil D(n)\frac32\rceil</math><ref>Formalized proof at https://github.com/rwst/Antihydra-Basics/blob/main/AntihydraBasics/Antihydra.lean</ref><ref>Formalized proof at https://github.com/rwst/Antihydra-Basics/blob/main/AntihydraBasics/Basics.lean</ref>, by <math>H(n)=D(n)+1</math>, which is of advantage because in the Odlyzko-Wilf paper<ref>https://scholar.archive.org/work/usw755p7rzgtbnfpmkliokwdfa/access/wayback/https://www.cambridge.org/core/services/aop-cambridge-core/content/view/13435C4851F0CA24F64E08357C9D64F1/S0017089500008272a.pdf/div-class-title-functional-iteration-and-the-josephus-problem-div.pdf</ref> they showed that <math display="inline">D(n)=\lfloor K\cdot(\frac32)^n\rfloor</math>, for some <math>K</math>. They showed this for starting value <math>D(0)=1</math> but the proof works perfectly for any starting value except that the constant <math>K</math> will be different<ref>Formalized proof at https://github.com/rwst/Antihydra-Basics/blob/main/AntihydraBasics/Constant.lean</ref>. This means that the halting problem is a question of the parities of <math>D(n)</math> (as hinted above). However, a similar question on the parity of <math display="inline">\lfloor \xi\cdot(\frac32)^n\rfloor</math> has come up with [https://en.wikipedia.org/wiki/Mahler%27s_3/2_problem Mahler's Z-number problem]. That problem is formulated as a condition on the fractional parts of <math display="inline">\xi\cdot(\frac32)^n</math> but this is just another form. The Z-number problem is a long-standing open question and it could be answered if it were proven that <math display="inline">\{ \xi\cdot(\frac32)^n\}</math>, with <math>\{x\}</math> the fractional part of <math>x</math>, is uniformly distributed (or equidistributed) over <math>(0,1)</math>. A positive answer to that could also mean that the parity vector of <math>D(n)</math> is normal and thus a random walk.

	== Code ==		== Code ==

Busy Beaver for lambda calculus

Tromp — Fri, 08 May 2026 19:47:12 GMT

General Recursive Function

Sligocki — Fri, 08 May 2026 16:54:20 GMT

Champions: BBµ(17) ≥ 2090

← Older revision		Revision as of 16:54, 8 May 2026
Line 238:		Line 238:
	\|-		\|-
	\|17		\|17
	\|≥ ~~1244~~		\|≥ 2090
	\|<math>M^{0}(R^{1~~}(C^{0}~~(~~S, Z^{0}),~~ R^{2}(S, R^{3}(P^~~{2}_{1}~~, C^{4}(R^{2}(S, R^{3}(~~P^{2}_{1}~~, P^~~{4}_{1}~~)), P^~~{4}_{4}~~, P^~~{4}_{2}~~)))))</math>		\|<math>M^0(C^1(R^2(P^1_1, R^3(P^2_1, R^4(R^3(R^2(S, C^3(S, P^3_2)), P^4_1), P^5_2))), P^1_1, S))</math>
	\|Shawn Ligocki [https://discord.com/channels/960643023006490684/1447627603698647303/~~1502007318382903438 7~~ May 2026]		\|Shawn Ligocki [https://discord.com/channels/960643023006490684/1447627603698647303/1502314241766588468 8 May 2026]
	\|		\|
	\|-		\|-
Line 256:		Line 256:
	\|-		\|-
	\|20		\|20
	\|~~≥ 1540~~		\|
	\|~~<math>C(AckDiag[0,Tri], K^0[2])</math>~~		\|
	\|~~Jacob Mandelson 9 Apr 2026~~		\|
	\|		\|
	\|-		\|-

Main Page

Sligocki — Fri, 08 May 2026 14:39:54 GMT

This Month in Beaver Research (TMBR): Update TMBR links

← Older revision		Revision as of 14:39, 8 May 2026
Line 75:		Line 75:
	[[:Category:This Month in Beaver Research\|This Month in Beaver Research]] (TMBR, pronounced "timber") is a monthly summary of Busy Beaver research progress. Here are the three most recent released entries:		[[:Category:This Month in Beaver Research\|This Month in Beaver Research]] (TMBR, pronounced "timber") is a monthly summary of Busy Beaver research progress. Here are the three most recent released entries:

			* [[TMBR: April 2026]]
	* [[TMBR: March 2026]]		* [[TMBR: March 2026]]
	* [[TMBR: February 2026]]		* [[TMBR: February 2026]]
	* [[TMBR: January 2026]]

	TMBR: May 2026 is currently work in progress, This Year in Beaver Research (TYBR) is a yearly summary of Busy Beaver research progress. Its first edition, [[TYBR: 2025]] is currently work in progress.		[[TMBR: May 2026]] is currently work in progress, This Year in Beaver Research (TYBR) is a yearly summary of Busy Beaver research progress. Its first edition, [[TYBR: 2025]] is currently work in progress.

	==Notes==		==Notes==
	<references />		<references />

← Older revision		Revision as of 19:47, 8 May 2026
(One intermediate revision by the same user not shown)
Line 554:		Line 554:
	* [[Busy Beaver for SKI calculus]]		* [[Busy Beaver for SKI calculus]]
	* https://oeis.org/A333479		* https://oeis.org/A333479
	* [https://~~tromp~~.~~github~~.io/~~blog~~/~~2026/01~~/28/~~largest-number-revised~~ The ~~largest number representable~~ in 64 ~~bits~~]. ~~28 Jan~~ 2026. John Tromp.		* [https://www.mdpi.com/1099-4300/28/5/494 The Largest Number Representable in 64 Bits]. 26 Apr 2026. John Tromp.
	* [https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861 Binary Lambda Calculus]. John Tromp.		* [https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861 Binary Lambda Calculus]. John Tromp.
	* https://github.com/tromp/AIT/tree/master/BB		* https://github.com/tromp/AIT/tree/master/BB
	* https://docs.google.com/spreadsheets/d/1jZ6TK9m3xmXUlC69727T-8WwvhALcsp8FrK6DzgThtw		* https://docs.google.com/spreadsheets/d/1jZ6TK9m3xmXUlC69727T-8WwvhALcsp8FrK6DzgThtw
	[[category:Functions]]		[[category:Functions]]