Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Computer Search Settles 90-Year-Old Math Problem

quantamagazine.org

Post reply on HN
Print view View original

11–19 of 19 posts

Re: Computer Search Settles 90-Year-Old Math Problem

#11

Post by 52-6F-62 »

jasonhong wrote: post #8
ghj wrote: post #2

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 abou…

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…

And as wonderfully illustrated by the conundrum surrounding https://www.google.com/search?rls=en&q=the+answer+to+life+th...

Re: Computer Search Settles 90-Year-Old Math Problem

#12

Post by CJefferson »

contravariant wrote: post #9
ghj wrote: post #2

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 abou…

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.

Further, most interesting theorems work "for all" things (graphs, lists, integers, whatever), so it requires some clever work to even make the problem finite.

Re: Computer Search Settles 90-Year-Old Math Problem

#13

Post by CJefferson »

faeyanpiraat wrote: post #3

The math might not be too complex but it still seems arcane magic to me. 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.

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.

Re: Computer Search Settles 90-Year-Old Math Problem

#14

Post by sumtechguy »

antman wrote: post #10
ghj wrote: post #2

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 abou…

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?

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

Re: Computer Search Settles 90-Year-Old Math Problem

#15

Post by strgcmc »

antman wrote: post #10
ghj wrote: post #2

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 abou…

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?

This 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 (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.

Re: Computer Search Settles 90-Year-Old Math Problem

#16

Post by fiddlerwoaroof »

antman wrote: post #10
ghj wrote: post #2

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 abou…

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?

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

Re: Computer Search Settles 90-Year-Old Math Problem

#17

Post by currymj »

antman wrote: post #10
ghj wrote: post #2

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 abou…

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?

Yes, 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_gam...

Re: Computer Search Settles 90-Year-Old Math Problem

#18

Post by umenthum »

antman wrote: post #10
ghj wrote: post #2

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 abou…

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?

I 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.htm...

Re: Computer Search Settles 90-Year-Old Math Problem

#19

Post by ford_o »

ghj wrote: post #2

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 abou…

How would you automatically find symmetries?
Post reply on HN