The proof that there is no finite projective plane of “order 10” (namely, one with 11 points per line) was a gory and large multi-part computation. The last phase, on a CRAY supercomputer (at low priority)
“…started running at IDA in the fall of 1986 and was to await completion in two to three years.”
C.W.H. Lam, The Search for a Finite Projective Plane of Order 10
before ultimately completing in 1988 (not without a final wrinkle, see the paper for more).
But I just learned there was an independent newer proof, this time using a SAT-solver, rather than a patchwork of custom code and by-hand computation!
- Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh, A SAT-based Resolution of Lam’s Problem arxiv:2012.04715, doi:10.1609/aaai.v35i5.16483
This is roughly analogous to how the original proof of the Four Colour Theorem was a much more bespoke operation, then the next proof in the 90s was more clever about removing the error-prone by-hand part. But! This is in fact the third independent proof of the non-existence result. There was an intermediate proof by Dominique Roy in 2011, but this was apparently still a matter of custom-written research code. A SAT-solver, on the other hand, is a generic tool, and their theory is intensely studied. Further, the software outputs a “proof certificate” at the end, rather than a boolean yes/no: this is a data object that can be fed into a piece of software that verifies the proof really does do what it says it does (you can get them here!). However, this is not yet a completely formalised proof (in the sense of how the Four Colour Theorem has been by now proved in the proof assistant Coq): there is some unformalised theorem(s) from the 1970s that are relied on. As you might imagine, the proof runtime took a lot less than 2 years of supercomputer time! Or rather, it took about 24 months on a standard personal computer, three months faster than Roy, compared to 30 months of compute time for Lam and collaborators in the 1980s, including their access to a CRAY machine.
theHigherGeometer 
I’m curious about if Lam et al’s computational work was redone using their method, how long it would take now on a workstation or network? By Moore’s law, you could say that there should be a speed up on the order of a thousand. It is good that an entirely different proof has been given here.
PS A projective plane of order 10 has 11 points on a line, not 9. ; )
LikeLike
Whoops! I got the +1 on the wrong side of the equation! I’ll fix that. I agree that updating the code for modern machinery would be good.
LikeLike