I wonder why progress has been so slow though. After the promising result decades ago where the Four Color Theorem was proven by a computer, I expected to see a lot more computer assisted proofs.
> They ultimately streamlined the search for a clique of size 128 so that instead of checking 2^39,000 configurations, their SAT solver only had to search about 1 billion (2^30)
Why is human insight needed for finding symmetries to make problems computationally tractable? Why can't this part be automated too? This must've been worked on for decades already, so is there a fundamental reason why computers can't do it?
EDIT: Also found some more technical links by one of the co-authors:
"The rapid advance of computers has helped dramatize this point, because computers and people are very different. For instance, when Appel and Haken completed a proof of the 4-color map theorem using a massive automatic computation, it evoked much controversy. I interpret the controversy as having little to do with doubt people had as to the veracity of the theorem or the correctness of the proof.
Rather, it reflected a continuing desire for human understanding of a proof, in
addition to knowledge that the theorem is true. On a more everyday level, it is common for people first starting to grapple with computers to make large-scale computations of things they might have done on a smaller scale by hand. They might print out a table of the first 10,000 primes, only to find that their printout isn’t something they really wanted after all. They discover by this kind of experience that what they really want is usually not some collection of “answers”—what they want is understanding."
It's almost the contrapositive of the law of small numbers that any large numbers tend to be very large, placing most of them beyond the reach of ordinary computers.
As for some “magic glasses” mathematical proving tool, it is probably inside the chocolate teapot on the other side of the sun.
I remember learning and using Coq in a similar 300-level CS course at my university, 10+ years ago.
Idk, but proof is certainly needed. If the code reduces by symmetry, that part of the code should be proven correct (too).
But the premise that a computer simulation solved the problem with a given reason that is too complicated to understood by humans, and require a separate computer program to verify is both fascinating and scary at the same time.
Edit: I just removed my comment because I failed at parsing this expression, and ended up replying to something you did not actually say.
There are Sudoku which (appear to be) beyond human ability to solve, but which computers will prove solvable within milliseconds, just by chewing through the options.