There Are No 4 Row High Orphans in Conway's Game of Life
Posted: June 11th, 2023, 2:51 pm
The proof consists of showing that there exists a set consisting of two columns from the parent generation and six "context" columns from the orphan candidate where any partial solution to an orphan candidate that matches an element of the set in it's last two columns and candidate context can be extended to some longer partial solution that also matches an element of the set in it's last two columns and candidate context.
The empty set trivially matches these conditions, but if a non-empty set can be found it is then possible to do induction on the length of the partial solutions and show that no orphan can exist.
An example of what I mean by extending to a longer partial solution:
The proof set I found has 21,767,045,299 elements. Finding this set is in principle as easy as starting with the set of all combinations and iteratively removing elements that don't fit the criteria until you're only left with the elements that do. But there are a couple of complications: In trying to prove an element belongs in the set you have the possibility of infinite loops, or even just taking an excessive amount of time. Therefore there needs to be some limit on how hard the program tries to prove an element belongs before giving up. I tried a number of possibilities here, and a simple distance-based cut off (at most 17 columns before finding a further element of the set) seemed to work as well as anything else. The other complication is that the self-referential nature of the proof set means that whenever an element is removed from the set the remaining elements will need to be re-checked for membership at some point. I think the number of passes through the set before convergence ended up being somewhere in the teens. The program does claw back a factor of two on the work required by taking advantage of symmetry, but it did end up taking about two months to run.
I've uploaded the program here:
https://codeberg.org/ajwade/orphan_disprover
The proof was completed with an earlier version of the program. I'm currently re-checking the proof with the latest version which should complete in the next day.
The artefact produced by the program is an 8GB file specifying the proof set so verification is difficult. I have added an --extend-solution option and have done some very limited spot-checks.
The empty set trivially matches these conditions, but if a non-empty set can be found it is then possible to do induction on the length of the partial solutions and show that no orphan can exist.
An example of what I mean by extending to a longer partial solution:
Code: Select all
enter target:
*******************************
**.*.***.* ***.*.***.*.***.*.**
*.***.*.***.*.***.*.***.*.***.*
*******************************
enter partial solution:
..**
.*..
*...
.*.*
*.**
....
Precondition:
**
(.., ******) is a member of the proof set: VERIFIED.
.. .*.***
.* ***.*.
** ******
..
Longer partial solution found:
..***.*
.*.....
*....*.
.*.**..
*.**..*
......*
Postcondition:
.*
(.., ******) is a member of the proof set: VERIFIED.
*. ***.*.
.. .*.***
.* ******
.*
I've uploaded the program here:
https://codeberg.org/ajwade/orphan_disprover
The proof was completed with an earlier version of the program. I'm currently re-checking the proof with the latest version which should complete in the next day.
The artefact produced by the program is an 8GB file specifying the proof set so verification is difficult. I have added an --extend-solution option and have done some very limited spot-checks.