User:RobinCodes/Next Steps - Revision history

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.

RobinCodes: BB(3,3) formalisation progress

2026-03-28T08:22:41Z

BB(3,3) formalisation progress

← Older revision		Revision as of 08:22, 28 March 2026
Line 43:		Line 43:
	1RB2LC1RC_2LC---2RB_2LA0LB0RA (758)</syntaxhighlight><small>The machines are in the same equivalence class and as such, achieve the same score on the susceptibility metric.</small>		1RB2LC1RC_2LC---2RB_2LA0LB0RA (758)</syntaxhighlight><small>The machines are in the same equivalence class and as such, achieve the same score on the susceptibility metric.</small>

	'''[[User:RobinCodes/Work on BB Domains#BB(3,3): 25 October 2025\|List of unverified proofs for individual machines (3 total proofs)]].'''		'''[[User:RobinCodes/Work on BB Domains#BB(3,3): 25 October 2025\|List of unverified proofs for individual machines (0 total proofs)]].'''

	== [[BB(6)]]: ==		== [[BB(6)]]: ==

RobinCodes: /* BB(6): */ Added e15 sim results

2026-03-10T06:17:59Z

BB(6):: Added e15 sim results

← Older revision		Revision as of 06:17, 10 March 2026
Line 46:		Line 46:

	== [[BB(6)]]: ==		== [[BB(6)]]: ==
	The goal is pretty straightforward in my opinion. Reduce the holdouts list to as far as we can, until all machines that are left seem way too hard (i.e. seemingly mathematically hard problems in their high-level behaviour), then write those problems up formally for potentially mathematicians to solve. Shorter-term goals include running the new FAR decider in a distributed-computation manner with higher params, and simulating all machines to 1e15. (Currently ~~239~~ holdouts)		The goal is pretty straightforward in my opinion. Reduce the holdouts list to as far as we can, until all machines that are left seem way too hard (i.e. seemingly mathematically hard problems in their high-level behaviour), then write those problems up formally for potentially mathematicians to solve. Shorter-term goals include running the new FAR decider in a distributed-computation manner with higher params, and simulating all machines to 1e15. (Currently 237 holdouts)

	=== Simulation ===		=== Simulation ===

← 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">