4 ms·
Yet another graph theory theorem falling to automated reasoning! I wonder why progress has been so slow though. After the promising result decades ago where th
by ghj 6y ago
Yet another graph theory theorem falling to automated reasoning!
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:
http://www.cs.cmu.edu/~mheule/talks/ijcar2020.pdf http://www.cs.cmu.edu/~mheule/talks/ijcar2020.pdf
http://www.cs.cmu.edu/~mheule/Keller/ http://www.cs.cmu.edu/~mheule/Keller/
- ohnoNotAgain321 6y agoHuman 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.
- tgv 6y ago> 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).
- jasonhong 6y agoFamed mathematician William Thurston has a good response here (from On Proof and Progress in Mathematics https://arxiv.org/pdf/math/9404236.pdf 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."
- 52-6F-62 6y agoAnd as wonderfully illustrated by the conundrum surrounding https://www.google.com/search?rls=en&q=the+answer+to+life+the+universe+and+everything https://www.google.com/search?rls=en&q=the+answer+to+life+th...
- contravariant 6y agoIf 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.
- CJefferson 6y agoFurther, most interesting theorems work "for all" things (graphs, lists, integers, whatever), so it requires some clever work to even make the problem finite.
- nick_kline 6y agoActually a lot of things get proved first for narrower domains (because it can be easier to prove,) and then get generalized to larger sets and maybe get really general! eventually. This was a great insight one of my college profs gave me.
- antman 6y agoI 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?
- sumtechguy 6y agoStart with the idea x=a+c. x can now be short hand for a+c. That may help? If you think of a theorem in the light that it is a giant function you can break it down that way too. Like sprintf is shorthand for the monster of bit of code that is sprintf.
- strgcmc 6y agoThis probably isn't a simple nor use-friendly intro, but it's pretty comprehensive at least: https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf (section 1.2 has the first minimal proof, although familiarity with formal logic is kind of a pre-req to properly parsing this style of writing) I remember learning and using Coq in a similar 300-level CS course at my university, 10+ years ago.
- fiddlerwoaroof 6y agoThe Little Prover might be a good choice: it’s about ACL2, which was used to prove various floating point implementations were correct. It’s a fairly accessible guide to proving theorems in this system.
- currymj 6y agoYes, this exists. it is called the "Natural Number Game" and interactively teaches you to use the Lean theorem prover to prove simple theorems about addition, multiplication, and so on. It runs in the browser. https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
- umenthum 6y agoI highly recommend Software Foundations Volume 1: Logical Foundations as an introduction to theorem proving in Coq. Try working through the first few chapters and see what you think: https://softwarefoundations.cis.upenn.edu/lf-current/toc.html https://softwarefoundations.cis.upenn.edu/lf-current/toc.htm...
- ford_o 6y agoHow would you automatically find symmetries?