User:RobinCodes/Next Steps - Revision history

RobinCodes: Fix hilarious mistake😇

2026-05-27T04:24:25Z

Fix hilarious mistake😇

← Older revision		Revision as of 04:24, 27 May 2026
Line 52:		Line 52:
	Apply new FAR decider as described in [https://discord.com/channels/960643023006490684/1239205785913790465/1472058729296822414 <nowiki>[1]</nowiki>] in a distributed computing effort.		Apply new FAR decider as described in [https://discord.com/channels/960643023006490684/1239205785913790465/1472058729296822414 <nowiki>[1]</nowiki>] in a distributed computing effort.

	The largest reduction possibility would be to create a decider for ~~Shit~~ Overflow Counters.		The largest reduction possibility would be to create a decider for Shift Overflow Counters.

	Spreadsheet of holdouts: [https://docs.google.com/spreadsheets/d/10y2aMp9yZVLyN-nXAxgA25rw4EA_lJqn3Vxy2kB-m-U/edit?gid=1330361301#gid=1330361301 spreadsheet]. There are 108 machines with completely unknown behaviour.		Spreadsheet of holdouts: [https://docs.google.com/spreadsheets/d/10y2aMp9yZVLyN-nXAxgA25rw4EA_lJqn3Vxy2kB-m-U/edit?gid=1330361301#gid=1330361301 spreadsheet]. There are 108 machines with completely unknown behaviour.

RobinCodes: /* BB(6): */ add paragraph

2026-05-27T04:14:02Z

BB(6):: add paragraph

← Older revision		Revision as of 04:14, 27 May 2026
Line 51:		Line 51:
	=== Deciders ===		=== Deciders ===
	Apply new FAR decider as described in [https://discord.com/channels/960643023006490684/1239205785913790465/1472058729296822414 <nowiki>[1]</nowiki>] in a distributed computing effort.		Apply new FAR decider as described in [https://discord.com/channels/960643023006490684/1239205785913790465/1472058729296822414 <nowiki>[1]</nowiki>] in a distributed computing effort.

			The largest reduction possibility would be to create a decider for Shit Overflow Counters.

	Spreadsheet of holdouts: [https://docs.google.com/spreadsheets/d/10y2aMp9yZVLyN-nXAxgA25rw4EA_lJqn3Vxy2kB-m-U/edit?gid=1330361301#gid=1330361301 spreadsheet]. There are 108 machines with completely unknown behaviour.		Spreadsheet of holdouts: [https://docs.google.com/spreadsheets/d/10y2aMp9yZVLyN-nXAxgA25rw4EA_lJqn3Vxy2kB-m-U/edit?gid=1330361301#gid=1330361301 spreadsheet]. There are 108 machines with completely unknown behaviour.

RobinCodes: updated bb2x5 progress

2026-04-10T09:18:45Z

updated bb2x5 progress

← Older revision		Revision as of 09:18, 10 April 2026
Line 3:		Line 3:

	== [[BB(2,5)]]: ==		== [[BB(2,5)]]: ==
	This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 11 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.		This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 10 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.

	'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys		'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys
Line 14:		Line 14:
	1RB4RA1LA4RB2LA_2LB3LA1RB2RA---		1RB4RA1LA4RB2LA_2LB3LA1RB2RA---
	1RB3RB3LA4LA2RB_2LB3RA---1RA1LA		1RB3RB3LA4LA2RB_2LB3RA---1RA1LA
	~~1RB3RB---4RA2RA_2LA2RA3LB4LB1LB~~
	1RB---3LB4RB0LA_2LB3LA3RB4RA0RA</syntaxhighlight><small>A few of them were [https://discord.com/channels/960643023006490684/1084047886494470185/1255556054587281569 categorized by @dyuan as “quasi-cascading”], but their individual behaviour is still unanalyzed.</small>		1RB---3LB4RB0LA_2LB3LA3RB4RA0RA</syntaxhighlight><small>A few of them were [https://discord.com/channels/960643023006490684/1084047886494470185/1255556054587281569 categorized by @dyuan as “quasi-cascading”], but their individual behaviour is still unanalyzed.</small>

RobinCodes: /* BB(2,5): */ Added all progress

2026-04-09T19:35:42Z

BB(2,5):: Added all progress

← Older revision		Revision as of 19:35, 9 April 2026
Line 3:		Line 3:

	== [[BB(2,5)]]: ==		== [[BB(2,5)]]: ==
	This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 12 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.		This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 11 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.

	'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys		'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys
Line 14:		Line 14:
	1RB4RA1LA4RB2LA_2LB3LA1RB2RA---		1RB4RA1LA4RB2LA_2LB3LA1RB2RA---
	1RB3RB3LA4LA2RB_2LB3RA---1RA1LA		1RB3RB3LA4LA2RB_2LB3RA---1RA1LA
	~~1RB3LA1LA2RB2RA_2LA4RA3LB1RA---~~
	1RB3RB---4RA2RA_2LA2RA3LB4LB1LB		1RB3RB---4RA2RA_2LA2RA3LB4LB1LB
	1RB---3LB4RB0LA_2LB3LA3RB4RA0RA</syntaxhighlight><small>A few of them were [https://discord.com/channels/960643023006490684/1084047886494470185/1255556054587281569 categorized by @dyuan as “quasi-cascading”], but their individual behaviour is still unanalyzed.</small>		1RB---3LB4RB0LA_2LB3LA3RB4RA0RA</syntaxhighlight><small>A few of them were [https://discord.com/channels/960643023006490684/1084047886494470185/1255556054587281569 categorized by @dyuan as “quasi-cascading”], but their individual behaviour is still unanalyzed.</small>

RobinCodes: /* BB(2,5): */ New non-analysed list

2026-04-09T18:25:24Z

BB(2,5):: New non-analysed list

RobinCodes: /* BB(3,3): */ Fixed numbers

2026-04-09T12:35:33Z

BB(3,3):: Fixed numbers

← Older revision		Revision as of 12:35, 9 April 2026
Line 33:		Line 33:

	== [[BB(3,3)]]: ==		== [[BB(3,3)]]: ==
	This domain is basically exhausted, and all 4 informal holdouts are what seem like mathematically very hard problems. In my opinion, the goal here is to prove the 3 holdouts solved informally by Legion via Longitudinal Analysis, then to describe the high-level behaviour of the remaining four machines, along with reasons for why we expect / don't expect them to halt, and with proofs of equivalency between machines 153, 758 and 531, 532.		This domain is basically exhausted, and all 4 informal holdouts are what seem like mathematically very hard problems. In my opinion, the goal here is to <s>prove the 3 holdouts solved informally by Legion via Longitudinal Analysis, then to</s> describe the high-level behaviour of the remaining four machines, along with reasons for why we expect / don't expect them to halt, and with Rocq proofs of equivalency between machines 153, 758 and machines 531, 532.

	Regardless;		Regardless;
Line 55:		Line 55:
	Apply new FAR decider as described in [https://discord.com/channels/960643023006490684/1239205785913790465/1472058729296822414 <nowiki>[1]</nowiki>] in a distributed computing effort.		Apply new FAR decider as described in [https://discord.com/channels/960643023006490684/1239205785913790465/1472058729296822414 <nowiki>[1]</nowiki>] in a distributed computing effort.

	Spreadsheet of holdouts: [https://docs.google.com/spreadsheets/d/10y2aMp9yZVLyN-nXAxgA25rw4EA_lJqn3Vxy2kB-m-U/edit?gid=1330361301#gid=1330361301 spreadsheet]. There are ~~106~~ machines with completely unknown behaviour.		Spreadsheet of holdouts: [https://docs.google.com/spreadsheets/d/10y2aMp9yZVLyN-nXAxgA25rw4EA_lJqn3Vxy2kB-m-U/edit?gid=1330361301#gid=1330361301 spreadsheet]. There are 108 machines with completely unknown behaviour.

	'''List of machines that are tractable to simulate until they very likely halt:''' [[User:RobinCodes/Machines at the Edge\|Machines at the Edge]]		'''List of machines that are tractable to simulate until they very likely halt:''' [[User:RobinCodes/Machines at the Edge\|Machines at the Edge]]

RobinCodes: /* BB(2,5): */ Update goal and numbers

2026-04-09T09:07:08Z

BB(2,5):: Update goal and numbers

← Older revision		Revision as of 09:07, 9 April 2026
Line 3:		Line 3:

	== [[BB(2,5)]]: ==		== [[BB(2,5)]]: ==
	This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts, apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 9 proofs and ~~2 proofs~~ of equivalence into ~~a formal language (~~Rocq).		This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 13 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.

	'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys		'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys

RobinCodes: /* BB(2,5): */ Removed TM from unanalysed list

2026-04-02T21:46:25Z

BB(2,5):: Removed TM from unanalysed list

RobinCodes: /* BB(2,5): */ BB(2,5) formalisation progress

2026-04-02T14:25:25Z

BB(2,5):: BB(2,5) formalisation progress

← Older revision		Revision as of 14:25, 2 April 2026
Line 31:		Line 31:
	1RB3LA1RA4LA2RA_2LA---1LA0RA3RB		1RB3LA1RA4LA2RA_2LA---1LA0RA3RB
	1RB2RB---0LB3LA_2LA2LB3RB4RB1LB		1RB2RB---0LB3LA_2LA2LB3RB4RB1LB
	</syntaxhighlight>'''[[User:RobinCodes/Work on BB Domains#BB(2,5): 25 October 2025\|List of unverified proofs for individual machines (9 total proofs)]].'''		</syntaxhighlight>'''[[User:RobinCodes/Work on BB Domains#BB(2,5): 25 October 2025\|List of unverified proofs for individual machines (6 total proofs)]].'''

	== [[BB(3,3)]]: ==		== [[BB(3,3)]]: ==

RobinCodes at 11:03, 1 April 2026

2026-04-01T11:03:58Z

← Older revision		Revision as of 11:03, 1 April 2026
Line 1:		Line 1:
	= Possible ~~next steps by domain~~ =		= Possible Next Steps =
	In this article I want to explore possible next steps in each domain and set forth goals about them.		In this article I want to explore possible next steps in each domain and set forth goals about them.

← Older revision		Revision as of 18:25, 9 April 2026
Line 3:		Line 3:

	== [[BB(2,5)]]: ==		== [[BB(2,5)]]: ==
	This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 13 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.		This domain is almost exhausted (especially decider-wise), though far from as much as 3x3. I think the goal here is to work on the holdouts (especially the 12 machines not yet inspected), apply deciders in a distributed-computation manner with high parameters (perhaps break the holdouts list into small pieces, that is, ~10 machines) and encourage people to run deciders with high parameters on them. Another important goal is to translate the 5 proofs and 1 proof of equivalence into Rocq.

	'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys		'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys
	1RB2RA3LA4LA2RB_2LA3RB---0RA1LA \| Chaotic via long. analysis		1RB2RA3LA4LA2RB_2LA3RB---0RA1LA \| Chaotic via long. analysis
	1RB---3RA2LA2RB_2LB3LA4LB4RA0RA \| Does not halt in 1.25e13		1RB---3RA2LA2RB_2LB3LA4LB4RA0RA \| Does not halt in 1.25e13
			1RB2RB3LA4LA1LA_2LB3RA---4RA1RB \| Does not halt in 3.4e13
	1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- \| Does not halt in 2e13		1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- \| Does not halt in 2e13
	1RB2RA4LA1RB4RB_1LB2LA3RA---0LB \| Does not halt in 5e13		1RB2RA4LA1RB4RB_1LB2LA3RA---0LB \| Does not halt in 5e13
	1RB---4LB0LA4RA_2LB2LA3RA4LB0RB		1RB---4LB0LA4RA_2LB2LA3RA4LB0RB
	1RB4RA1LA4RB2LA_2LB3LA1RB2RA---		1RB4RA1LA4RB2LA_2LB3LA1RB2RA---
	~~1RB2RB3LA4LA1LA_2LB3RA---4RA1RB~~
	1RB3RB3LA4LA2RB_2LB3RA---1RA1LA		1RB3RB3LA4LA2RB_2LB3RA---1RA1LA
	~~1RB4RB4RA1LA3LA_1LB2LA3RB2RB---~~
	1RB3LA1LA2RB2RA_2LA4RA3LB1RA---		1RB3LA1LA2RB2RA_2LA4RA3LB1RA---
	1RB3RB---4RA2RA_2LA2RA3LB4LB1LB		1RB3RB---4RA2RA_2LA2RA3LB4LB1LB

← Older revision		Revision as of 21:46, 2 April 2026
Line 7:		Line 7:
	'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys		'''List of machines which have not yet been manually inspected.'''<syntaxhighlight lang="html">1RB2RA3LA4LA2RB_2LA3RA---0RA1LA \| Chaotic via long. analysis \| Notes by mxdys
	1RB2RA3LA4LA2RB_2LA3RB---0RA1LA \| Chaotic via long. analysis		1RB2RA3LA4LA2RB_2LA3RB---0RA1LA \| Chaotic via long. analysis
	~~1RB2LA0RB4LB0LA_1LA3LA1RA4RA--- \| Does not halt in 1e13~~
	1RB---3RA2LA2RB_2LB3LA4LB4RA0RA \| Does not halt in 1.25e13		1RB---3RA2LA2RB_2LB3LA4LB4RA0RA \| Does not halt in 1.25e13
	1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- \| Does not halt in 2e13		1RB3RB1LA2LA3RA_1LB2RA4RB0LA--- \| Does not halt in 2e13
Line 60:		Line 59:
	'''List of machines that are tractable to simulate until they very likely halt:''' [[User:RobinCodes/Machines at the Edge\|Machines at the Edge]]		'''List of machines that are tractable to simulate until they very likely halt:''' [[User:RobinCodes/Machines at the Edge\|Machines at the Edge]]

	'''List of machines that "should be solvable/easy": [https://discord.com/channels/960643023006490684/1460495597386731643/1460495597386731643 More extensive list, forum here]'''<syntaxhighlight lang="text">		'''List of machines* that "should be solvable/easy": [https://discord.com/channels/960643023006490684/1460495597386731643/1460495597386731643 More extensive list, forum here]'''<syntaxhighlight lang="text">
	1RB1LE_0RC1RC_0RD0RB_1RE0RF_1LA0LE_---1RB		1RB1LE_0RC1RC_0RD0RB_1RE0RF_1LA0LE_---1RB
	1RB0LE_1LC1LB_0RD0LC_1RA0RE_1RF1RD_0RA---		1RB0LE_1LC1LB_0RD0LC_1RA0RE_1RF1RD_0RA---
Line 83:		Line 82:
	1RB1RD_1LC0LE_1RA0LB_1RA1RF_0RA0RC_1RE---		1RB1RD_1LC0LE_1RA0LB_1RA1RF_0RA0RC_1RE---
	1RB1LB_1LC0RD_0LE1LA_0RF1RA_1LE0LA_---0RB		1RB1LB_1LC0RD_0LE1LA_0RF1RA_1LE0LA_---0RB
	</syntaxhighlight>'''Top 10 machines which visit the least amount of cells in 1 billion steps: ([https://discord.com/channels/960643023006490684/1239205785913790465/1434394395653836830 src]) ([https://wiki.bbchallenge.org/w/images/5/5b/Least_cells_visited_2.txt Full list])'''		</syntaxhighlight>'''Top 10 machines* which visit the least amount of cells in 1 billion steps: ([https://discord.com/channels/960643023006490684/1239205785913790465/1434394395653836830 src]) ([https://wiki.bbchallenge.org/w/images/5/5b/Least_cells_visited_2.txt Full list])'''

	<small>[https://wiki.bbchallenge.org/w/images/e/ef/Least_cells_visited.txt List for 1 million steps, some machines may be missing] ([https://discord.com/channels/960643023006490684/1239205785913790465/1433693493775171654 src])</small><syntaxhighlight lang="html">		<small>[https://wiki.bbchallenge.org/w/images/e/ef/Least_cells_visited.txt List for 1 million steps, some machines may be missing] ([https://discord.com/channels/960643023006490684/1239205785913790465/1433693493775171654 src])</small><syntaxhighlight lang="html">