Computer Search Settles 90-Year-Old Math Problem

Human understanding of cognition is not yet at a level that enables the creation of a program or system for general automated theorem proving. Much work has been required to create existing systems for very narrow problems. Technology has not reached a level where artificial intelligence systems can undergo the equivalent of millions of years of evolution to achieve an equivalence to general human intelligence; this may not even be achievable.

As for some “magic glasses” mathematical proving tool, it is probably inside the chocolate teapot on the other side of the sun.

> Why is human insight needed

Idk, but proof is certainly needed. If the code reduces by symmetry, that part of the code should be proven correct (too).

Famed mathematician William Thurston has a good response here (from On Proof and Progress in Mathematics https://arxiv.org/pdf/math/9404236.pdf):

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

If you ask me the relative rarity of computer assisted (brute force) proofs is because it is only useful in the unlikely scenario that the number of cases to check is too large for humans but small enough to be computationally tractable.

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.

I can't wrap myself around how theorem provers work. Is there something like a beginner tutorial with examples from simple uses? And which theorem prover would be intuitive for an introduction to this space?

How would you automatically find symmetries?

>solved the problem with a given reason

Edit: I just removed my comment because I failed at parsing this expression, and ended up replying to something you did not actually say.

Very interesting result indeed. The key was that the researchers developed an algorithm to automatically improve the efficiency of their SAT search - the 200 GB "proof" was just the logic equating their efficient SAT search with the original SAT problem - the output of their algorithm. The real magic was in devising this algorithm.

Once you have a finite problem (which usually requires human human), computers can just chew through cases.

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.