- This result has effectively only two colours: "coloured" and "not coloured".
- This relates to an infinite continuous plane of points rather than a finite, discrete set.
- This has a notion of distance, whereas the four-colour theorem is more about connectivity.
That said, the idea of using a computer to aid a proof did also occur in the original proof of the four colour theorem.
The Quanta article rushed through some aspects of our work, so I'll try to use this opportunity to elaborate. This has a very small target audience: those who have skimmed the original post, and would like to go a bit deeper. AMA!
Alice gives us a unit distance avoiding set. We want to prove that its density is less than 1/4. Independently, Bob gives us an n element point set on the plane. We use it to translate Alice's set into n translated versions, take all 2^n possible n-wise intersections between these translations, and write up a tricky and huge linear program for the densities of these intersections. Solving that LP gives us an upper bound for the density of Alice's set.
Bob's finite set works for any set coming from Alice. So we have reduced Erdős's problem to finding a finite set with the property that its LP objective is less than 1/4. That is the search problem that we solve by starting from the 7 element Moser spindle, and incrementally adding points to it, guided by a modified beam search. The LP size is exponential in the number of points, but before exhausting memory and/or CPU budget, the search has come back with a 23 element set that is a witness to the fact that the Erdős's conjecture is true. (It is the weird graph in supplementary material https://bit.ly/unit-distances )
