TMBR: May 2026 - Revision history

Tjligocki: Modified the appearance of some link text from the raw link to text.

2026-10-07T03:42:33Z

Modified the appearance of some link text from the raw link to text.

← Older revision		Revision as of 03:42, 7 October 2026
Line 42:		Line 42:
	* TODO: BB Bignum Bakeoff		* TODO: BB Bignum Bakeoff

	* GPU deciders: The original discussion of this starts with a ~~discord post,~~ https://discord.com/channels/960643023006490684/960643023530762343/1507544052185301092, where David SG announced some work he was doing with GPU deciders. Subsequently, they shared a ~~Github repo,~~ https://github.com/David5768/David-BB7-GPU-Deciders, and contributed some new results for BB(6) TMs. TODO: List BB(6) TMs decided, other domains, additional details.		* GPU deciders: The original discussion of this starts with a [https://discord.com/channels/960643023006490684/960643023530762343/1507544052185301092 discord post], where David SG announced some work he was doing with GPU deciders. Subsequently, they shared a [https://github.com/David5768/David-BB7-GPU-Deciders Github repo], and contributed some new results for BB(6) TMs. TODO: List BB(6) TMs decided, other domains, additional details.

	* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others, which could eventually be useful for creating [[Logical independence\|axiomatically undecidable]] machines.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>		* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others, which could eventually be useful for creating [[Logical independence\|axiomatically undecidable]] machines.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>

Tjligocki: /* Misc */ Fleshed out the GPU deciders TODO with some details and other possible TODOs that may not be necessary.

2026-10-06T22:53:13Z

Misc: Fleshed out the GPU deciders TODO with some details and other possible TODOs that may not be necessary.

← Older revision		Revision as of 22:53, 6 October 2026
Line 41:		Line 41:
	* 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>		* 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>
	* TODO: BB Bignum Bakeoff		* TODO: BB Bignum Bakeoff
	* ~~TODO~~: GPU deciders
			* GPU deciders: The original discussion of this starts with a discord post, https://discord.com/channels/960643023006490684/960643023530762343/1507544052185301092, where David SG announced some work he was doing with GPU deciders. Subsequently, they shared a Github repo, https://github.com/David5768/David-BB7-GPU-Deciders, and contributed some new results for BB(6) TMs. TODO: List BB(6) TMs decided, other domains, additional details.

	* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others, which could eventually be useful for creating [[Logical independence\|axiomatically undecidable]] machines.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>		* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others, which could eventually be useful for creating [[Logical independence\|axiomatically undecidable]] machines.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>

HelpMe: corrected possible cryptid

2026-10-05T08:53:05Z

corrected possible cryptid

← Older revision		Revision as of 08:53, 5 October 2026
Line 14:		Line 14:
	** 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.
	* On 5 May, Shawn implemented a size 133 GRF that non-trivially halts iff there is a counter-example to Fermat's Last Theorem: [https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/fermat.mgrf fermat.mgrf].<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501235408913305663]</sup> Note that since Fermat's Last Theorem is true, this GRF does not halt; however, this GRF is still of interest due to the complexity of the proof of the theorem.		* On 5 May, Shawn implemented a size 133 GRF that non-trivially halts iff there is a counter-example to Fermat's Last Theorem: [https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/fermat.mgrf fermat.mgrf].<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501235408913305663]</sup> Note that since Fermat's Last Theorem is true, this GRF does not halt; however, this GRF is still of interest due to the sheer complexity and length of the proof of the theorem.
	* On 6 May, Shawn found a chaotic (potentially Cryptid) size 15 GRF: <code>C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S)</code>.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501444301245382707]</sup>		* On 6 May, Shawn found a chaotic (potentially Cryptid) size 16 GRF: <code>M(C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S))</code>.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501444301245382707]</sup>
	* All M(PRF) GRFs were decided up to size 12 with max score 5.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>		* All M(PRF) GRFs were decided up to size 12 with max score 5.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>
	* All PRFs were decided up to size 22 with max score <math>\approx 2^{2^{230}}</math>. All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>		* All PRFs were decided up to size 22 with max score <math>\approx 2^{2^{230}}</math>. All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>

HelpMe: omg apparently the bugged ennumeration erased all of that progress in bbcs(11). also fixed citation numbering

2026-10-03T17:24:06Z

omg apparently the bugged ennumeration erased all of that progress in bbcs(11). also fixed citation numbering

← Older revision		Revision as of 17:24, 3 October 2026
Line 32:		Line 32:
	* On 6 May, sheep discovered a new champion for BBCS(21)<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1501545706601578527]</sup> and on 11 May a new champion for BBCS(25).<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1503294458861719574]</sup>		* On 6 May, sheep discovered a new champion for BBCS(21)<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1501545706601578527]</sup> and on 11 May a new champion for BBCS(25).<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1503294458861719574]</sup>
	* On 13 May, sheep proved CounterScript Turing-complete via a translation from B*olfuck to Counterscript.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1504113618231492628]</sup> 2 days later, she showed that CounterScript restricted to 3 registers was also Turing-complete.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1504770973684203581]</sup>		* On 13 May, sheep proved CounterScript Turing-complete via a translation from B*olfuck to Counterscript.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1504113618231492628]</sup> 2 days later, she showed that CounterScript restricted to 3 registers was also Turing-complete.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1504770973684203581]</sup>
	* On 23 May, Azerty enumerated BBCS(11).<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1507711168465338398]</sup> All 39 holdouts were shown to be non-halting, proving BBCS(11) = 20.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1554807350811168868][https://discord.com/channels/960643023006490684/1484108791636033659/1507711168465338398]</sup>
	[[Fractran]]:		[[Fractran]]:
	* On 28 May, @-d began enumerating BBf(23).<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1509348792330358965]</sup> The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1510749997392724190]</sup>		* On 28 May, @-d began enumerating BBf(23).<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1509348792330358965]</sup> The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1510749997392724190]</sup>
Line 92:		Line 91:
	**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.
	**Using FAR, Andrew Ducharme further reduced the number of holdouts from 439,120 to '''418,127''', a '''4.78%''' reduction.		**Using FAR, Andrew Ducharme further reduced the number of holdouts from 439,120 to '''418,127''', a '''4.78%''' reduction.
	**Using some mxdys deciders, Andrew Ducharme continued reducing the number of holdouts through May 17, from 418,127 to '''413,513''' (a '''1.10%''' reduction).<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1505277282648981504 ~~<nowiki>[13]</nowiki>~~][https://discord.com/channels/960643023006490684/1084047886494470185/1506063539498913934 ~~<nowiki>[14]</nowiki>~~][https://discord.com/channels/960643023006490684/1084047886494470185/1507614139563118694 ~~<nowiki>[15]</nowiki>~~][https://discord.com/channels/960643023006490684/1084047886494470185/1508623369967370472 ~~<nowiki>[16]</nowiki>~~]</sup>		**Using some mxdys deciders, Andrew Ducharme continued reducing the number of holdouts through May 17, from 418,127 to '''413,513''' (a '''1.10%''' reduction).<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1505277282648981504][https://discord.com/channels/960643023006490684/1084047886494470185/1506063539498913934][https://discord.com/channels/960643023006490684/1084047886494470185/1507614139563118694][https://discord.com/channels/960643023006490684/1084047886494470185/1508623369967370472]</sup>
	*[[BB(2,7)]]		*[[BB(2,7)]]
	** Terry Ligocki enumerated 130K more subtasks, increasing the number of holdouts to '''1,087,732,936'''. A total of 350K subtasks out of the 1 million subtasks (or '''35%''') have been enumerated.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1492652604088516659 ~~<nowiki>[17]</nowiki>~~]</sup>		** Terry Ligocki enumerated 130K more subtasks, increasing the number of holdouts to '''1,087,732,936'''. A total of 350K subtasks out of the 1 million subtasks (or '''35%''') 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 Adjacent */

2026-10-01T15:41:07Z

BB Adjacent

← Older revision		Revision as of 15:41, 1 October 2026
Line 20:		Line 20:
	[[SKI Calculus]]:		[[SKI Calculus]]:
	* On 7 May, Δ⁵ discovered some tetrational (size 15) and pentational (size 19) terms in the SKI calculus,<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=prev&oldid=7455]</sup> and some small champions for [[SKI Calculus#SK calculus\|Ξ₀<sub>SK</sub>(n)]] for sizes 9 to 15.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7455]</sup>		* On 7 May, Δ⁵ discovered some tetrational (size 15) and pentational (size 19) terms in the SKI calculus,<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=prev&oldid=7455]</sup> and some small champions for [[SKI Calculus#SK calculus\|Ξ₀<sub>SK</sub>(n)]] for sizes 9 to 15.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7455]</sup>
	* By 7 May, an unknown person translated 2014MELO03's lambda calculus champion to SKI calculus, proving the bound Ξ₀(25) > [[Graham's number]]<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7461]</sup> (falsely attributed to 2014MELO03).		* By 7 May, an unknown person (probably tromp) translated 2014MELO03's lambda calculus champion to SKI calculus, proving the bound Ξ₀(25) > [[Graham's number]]<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7461]</sup> (falsely attributed to 2014MELO03).
	* On 15 May, Δ⁵ proved the bound Ξ₀(22) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7521]</sup>		* On 15 May, Δ⁵ proved the bound Ξ₀(22) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7521]</sup>
	* On 19 May, Δ⁵ proved Ξ₀(6) = 17 and Ξ₀<sub>SK</sub>(6) = 10.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7543]</sup>		* On 19 May, Δ⁵ proved Ξ₀(6) = 17 and Ξ₀<sub>SK</sub>(6) = 10.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7543]</sup>

Δ⁵ at 12:18, 30 September 2026

2026-09-30T12:18:01Z

← Older revision		Revision as of 12:18, 30 September 2026
Line 20:		Line 20:
	[[SKI Calculus]]:		[[SKI Calculus]]:
	* On 7 May, Δ⁵ discovered some tetrational (size 15) and pentational (size 19) terms in the SKI calculus,<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=prev&oldid=7455]</sup> and some small champions for [[SKI Calculus#SK calculus\|Ξ₀<sub>SK</sub>(n)]] for sizes 9 to 15.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7455]</sup>		* On 7 May, Δ⁵ discovered some tetrational (size 15) and pentational (size 19) terms in the SKI calculus,<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=prev&oldid=7455]</sup> and some small champions for [[SKI Calculus#SK calculus\|Ξ₀<sub>SK</sub>(n)]] for sizes 9 to 15.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7455]</sup>
	* By 7 May, an unknown person ~~proved~~ the bound Ξ₀(25) > [[Graham's number]]<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7461]</sup> (falsely attributed to 2014MELO03).		* By 7 May, an unknown person translated 2014MELO03's lambda calculus champion to SKI calculus, proving the bound Ξ₀(25) > [[Graham's number]]<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7461]</sup> (falsely attributed to 2014MELO03).
	* On 15 May, Δ⁵ proved the bound Ξ₀(22) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7521]</sup>		* On 15 May, Δ⁵ proved the bound Ξ₀(22) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7521]</sup>
	* On 19 May, Δ⁵ proved Ξ₀(6) = 17 and Ξ₀<sub>SK</sub>(6) = 10.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7543]</sup>		* On 19 May, Δ⁵ proved Ξ₀(6) = 17 and Ξ₀<sub>SK</sub>(6) = 10.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7543]</sup>
	* On 22 May, Δ⁵ discovered smaller tetrational (size 13) and pentational (size 17) terms in the SKI calculus, and proved the bound Ξ₀(20) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7583]</sup>		* On 22 May, Δ⁵ discovered smaller tetrational (size 13) and pentational (size 17) terms in the SKI calculus, and 50_ft_locker proved the bound Ξ₀(20) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7583]</sup>
	* On 23 May, ~~Azerty~~ discovered new Ξ₀<sub>SK</sub>(n) champions for sizes 7 to 12<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7600]</sup> (and Ξ₀(n) champions for sizes 7 to 10<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7613]</sup>), as well as a Ξ₀(11) champion 2 days later.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7614]</sup>		* On 23 May, Boone discovered new Ξ₀<sub>SK</sub>(n) champions for sizes 7 to 12<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7600]</sup> (and Ξ₀(n) champions for sizes 7 to 10<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7613]</sup>), as well as a Ξ₀(11) champion 2 days later.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7614]</sup>
	* On 25 May, Azerty introduced the Busy Beaver function for the BCKW system.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7633]</sup>		* On 25 May, Azerty introduced the Busy Beaver function for the BCKW system.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7633]</sup>
	* On 26 May, Δ⁵ discovered some tetrational (size 7) and Ackeramnn-growth (size 11) terms in the [[SKI Calculus#BCKW system\|BCKW system]], and proved the bound Ξ₀<sub>BCKW</sub>(12) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7639]</sup>		* On 26 May, Δ⁵ discovered some tetrational (size 7) and Ackeramnn-growth (size 11) terms in the [[SKI Calculus#BCKW system\|BCKW system]], and proved the bound Ξ₀<sub>BCKW</sub>(12) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7639]</sup>

HelpMe: added champions for combinator busy beavers, BBCS(10) was proven last month. elaborate on why FLT is very interesting and we should worship the theorem

2026-09-30T11:54:23Z

added champions for combinator busy beavers, BBCS(10) was proven last month. elaborate on why FLT is very interesting and we should worship the theorem

← Older revision		Revision as of 11:54, 30 September 2026
Line 14:		Line 14:
	** 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.
	* On 5 May, Shawn implemented a size 133 GRF that halts iff there ~~was~~ a counter-example to Fermat's Last Theorem: [https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/fermat.mgrf fermat.mgrf].<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501235408913305663]</sup>		* On 5 May, Shawn implemented a size 133 GRF that non-trivially halts iff there is a counter-example to Fermat's Last Theorem: [https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/fermat.mgrf fermat.mgrf].<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501235408913305663]</sup> Note that since Fermat's Last Theorem is true, this GRF does not halt; however, this GRF is still of interest due to the complexity of the proof of the theorem.
	* On 6 May, Shawn found a chaotic (potentially Cryptid) size 15 GRF: <code>C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S)</code>.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501444301245382707]</sup>		* On 6 May, Shawn found a chaotic (potentially Cryptid) size 15 GRF: <code>C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S)</code>.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501444301245382707]</sup>
	* All M(PRF) GRFs were decided up to size 12 with max score 5.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>		* All M(PRF) GRFs were decided up to size 12 with max score 5.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>
	* All PRFs were decided up to size 22 with max score <math>\approx 2^{2^{230}}</math>. All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>		* All PRFs were decided up to size 22 with max score <math>\approx 2^{2^{230}}</math>. All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>
	[[SKI Calculus]]:		[[SKI Calculus]]:
	* ~~Many new champions were~~ discovered ~~for~~ the ~~Busy Beaver variants of~~ SKI calculus, [[SKI Calculus#SK calculus\|SK calculus]] and [[SKI Calculus#BCKW system\|BCKW system]].		* On 7 May, Δ⁵ discovered some tetrational (size 15) and pentational (size 19) terms in the SKI calculus,<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=prev&oldid=7455]</sup> and some small champions for [[SKI Calculus#SK calculus\|Ξ₀<sub>SK</sub>(n)]] for sizes 9 to 15.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7455]</sup>
			* By 7 May, an unknown person proved the bound Ξ₀(25) > [[Graham's number]]<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7461]</sup> (falsely attributed to 2014MELO03).
			* On 15 May, Δ⁵ proved the bound Ξ₀(22) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7521]</sup>
			* On 19 May, Δ⁵ proved Ξ₀(6) = 17 and Ξ₀<sub>SK</sub>(6) = 10.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7543]</sup>
			* On 22 May, Δ⁵ discovered smaller tetrational (size 13) and pentational (size 17) terms in the SKI calculus, and proved the bound Ξ₀(20) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7583]</sup>
			* On 23 May, Azerty discovered new Ξ₀<sub>SK</sub>(n) champions for sizes 7 to 12<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7600]</sup> (and Ξ₀(n) champions for sizes 7 to 10<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7613]</sup>), as well as a Ξ₀(11) champion 2 days later.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7614]</sup>
			* On 25 May, Azerty introduced the Busy Beaver function for the BCKW system.<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7633]</sup>
			* On 26 May, Δ⁵ discovered some tetrational (size 7) and Ackeramnn-growth (size 11) terms in the [[SKI Calculus#BCKW system\|BCKW system]], and proved the bound Ξ₀<sub>BCKW</sub>(12) > [[Graham's number]].<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7639]</sup>
			* On 29 May, Δ⁵ discovered an infinite family of terms in the SKI calculus with normal form growth rate f<sub>ω⋅2</sub>(n).<sup>[https://wiki.bbchallenge.org/w/index.php?title=SKI_Calculus&diff=next&oldid=7700]</sup>
	[[CounterScript]]:		[[CounterScript]]:
	* On 1 May, discord user sheep discovered a BBCS(65) champion beating [[Graham's number]].<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1499727568763617381]</sup> On 3 May, sheep improved this champion [https://discord.com/channels/960643023006490684/1484108791636033659/1509179336136327310 to size 64].<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1500384646922240084]<sup>		* On 1 May, discord user sheep discovered a BBCS(65) champion beating [[Graham's number]].<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1499727568763617381]</sup> On 3 May, sheep improved this champion [https://discord.com/channels/960643023006490684/1484108791636033659/1509179336136327310 to size 64].<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1500384646922240084]<sup>
	* BBCS(10) was shown to be exactly 16.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1500430734920515736]</sup>
	* On 6 May, sheep discovered a new champion for BBCS(21)<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1501545706601578527]</sup> and on 11 May a new champion for BBCS(25).<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1503294458861719574]</sup>		* On 6 May, sheep discovered a new champion for BBCS(21)<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1501545706601578527]</sup> and on 11 May a new champion for BBCS(25).<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1503294458861719574]</sup>
	* On 16 May, Azerty enumerated BBCS(11). [~~TODO~~: ~~bug found, may have~~ to be ~~removed]~~<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/~~1505131900023607388~~]</sup>		* On 13 May, sheep proved CounterScript Turing-complete via a translation from B*olfuck to Counterscript.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1504113618231492628]</sup> 2 days later, she showed that CounterScript restricted to 3 registers was also Turing-complete.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1504770973684203581]</sup>
			* On 23 May, Azerty enumerated BBCS(11).<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1507711168465338398]</sup> All 39 holdouts were shown to be non-halting, proving BBCS(11) = 20.<sup>[https://discord.com/channels/960643023006490684/1484108791636033659/1554807350811168868][https://discord.com/channels/960643023006490684/1484108791636033659/1507711168465338398]</sup>
	[[Fractran]]:		[[Fractran]]:
	* On 28 May, @-d began enumerating BBf(23).<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1509348792330358965]</sup> The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1510749997392724190]</sup>		* On 28 May, @-d began enumerating BBf(23).<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1509348792330358965]</sup> The enumeration was completed by 31 May, leaving an initial 790,335 holdouts, which where reduced to 29,250 holdouts.<sup>[https://discord.com/channels/960643023006490684/1438019511155691521/1510749997392724190]</sup>
Line 70:		Line 78:
	\|22.87%		\|22.87%
	\|}		\|}

			* [[BB(7)]]
			** David SG begins directly simulating the 17.8 million BB(7) holdouts using one of their servers, simulating over 1 million holdouts to halting.<sup>[https://discord.com/channels/960643023006490684/1369339127652159509/1509784217515462747]</sup>

	*[[BB(2,5)]]		*[[BB(2,5)]]
	**[https://discord.com/channels/960643023006490684/1259770421046411285/1510322250769760376 Andrew Ducharme found a FAR solution for a machine], which previously had an informal nonhalting argument. On June 1st, [https://discord.com/channels/960643023006490684/1259770421046411285/1510867717194911874 mxdys provided the Rocq proof], reducing the Rocq-holdout count to '''65'''.		**[https://discord.com/channels/960643023006490684/1259770421046411285/1510322250769760376 Andrew Ducharme found a FAR solution for a machine], which previously had an informal nonhalting argument. On June 1st, [https://discord.com/channels/960643023006490684/1259770421046411285/1510867717194911874 mxdys provided the Rocq proof], reducing the Rocq-holdout count to '''65'''.

Tlonuqbar: clarifying importance of Legion's project for BB

2026-07-28T19:56:22Z

clarifying importance of Legion's project for BB

← Older revision		Revision as of 19:56, 28 July 2026
Line 1:		Line 1:
	{{TMBRnav\|April 2026\|June 2026}}		{{TMBRnav\|April 2026\|June 2026}}

	''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).''		''This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).'' [[:Category:This Month in Beaver Research\|This Month in Beaver Research]] for May 2026.

	== BB Adjacent ==		== BB Adjacent ==
Line 35:		Line 35:
	* TODO: BB Bignum Bakeoff		* TODO: BB Bignum Bakeoff
	* TODO: GPU deciders		* TODO: GPU deciders
	* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>		* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others, which could eventually be useful for creating [[Logical independence\|axiomatically undecidable]] machines.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>

	== Holdouts ==		== Holdouts ==

Sligocki: /* Misc */ Add Legion's Axiom of Infinity results.

2026-07-18T23:53:08Z

Misc: Add Legion's Axiom of Infinity results.

← Older revision		Revision as of 23:53, 18 July 2026
Line 4:		Line 4:

	== BB Adjacent ==		== BB Adjacent ==
	[[General Recursive Function\|General Recursive Functions]]: ~~TODO: Further progress~~		[[General Recursive Function\|General Recursive Functions]]:

	* Some new champions were found:		* Some new champions were found:
Line 35:		Line 35:
	* TODO: BB Bignum Bakeoff		* TODO: BB Bignum Bakeoff
	* TODO: GPU deciders		* TODO: GPU deciders
			* LegionMammal shared exploration they have made into searching for alternative "Axiom of Infinity" like statements and which ones imply which others.<sup>[https://discord.com/channels/960643023006490684/960643023530762341/1488636445148184729]</sup>

	== Holdouts ==		== Holdouts ==

Sligocki: Finish up GRF notes for May

2026-07-18T23:18:00Z

Finish up GRF notes for May

← Older revision		Revision as of 23:18, 18 July 2026
Line 16:		Line 16:
	* On 5 May, Shawn implemented a size 133 GRF that halts iff there was a counter-example to Fermat's Last Theorem: [https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/fermat.mgrf fermat.mgrf].<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501235408913305663]</sup>		* On 5 May, Shawn implemented a size 133 GRF that halts iff there was a counter-example to Fermat's Last Theorem: [https://github.com/sligocki/etc/blob/main/gen_rec/mgrf/fermat.mgrf fermat.mgrf].<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501235408913305663]</sup>
	* On 6 May, Shawn found a chaotic (potentially Cryptid) size 15 GRF: <code>C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S)</code>.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501444301245382707]</sup>		* On 6 May, Shawn found a chaotic (potentially Cryptid) size 15 GRF: <code>C(R(S, R(C(S, P(2,1)), C(R(P(1,1), P(3,1)), P(4,2), P(4,1)))), P(1,1), S)</code>.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1501444301245382707]</sup>
			* All M(PRF) GRFs were decided up to size 12 with max score 5.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>
			* All PRFs were decided up to size 22 with max score <math>\approx 2^{2^{230}}</math>. All except 11 were decided by direct simulation, but 11 overflowed u64 and needed to be evaluated by more clever programs.<sup>[https://discord.com/channels/960643023006490684/1447627603698647303/1508151420258484354]</sup>
	[[SKI Calculus]]:		[[SKI Calculus]]:
	* Many new champions were discovered for the Busy Beaver variants of SKI calculus, [[SKI Calculus#SK calculus\|SK calculus]] and [[SKI Calculus#BCKW system\|BCKW system]].		* Many new champions were discovered for the Busy Beaver variants of SKI calculus, [[SKI Calculus#SK calculus\|SK calculus]] and [[SKI Calculus#BCKW system\|BCKW system]].