A SAT Attack on the Erdos Discrepancy Conjecture

April 12, 2014 8:55 AM

Computers are providing solutions to math problems that we can't check - "A computer has solved the longstanding Erdős discrepancy problem! Trouble is, we have no idea what it's talking about — because the solution, which is as long as all of Wikipedia's pages combined, is far too voluminous for us puny humans to confirm." (via; previously ;)
posted by kliuless (24 comments total)

The singularity has arrived! Huzzah!


Actually this is an interesting problem. About the best you could do is have independent parties create proof checkers that walked through the solution. Which when you get down to it may have a higher accuracy rate for less voluminous proofs as well.
posted by Tell Me No Lies at 9:07 AM on April 12, 2014 [3 favorites]

There is absolutely elegance in the brute force solution. It's just not as pretty on paper.
posted by three blind mice at 9:18 AM on April 12, 2014 [3 favorites]

Now, here's a question.

Would it be possible to create a sort of AI conjecture-maker entity? An AI that knows how all these various parts relate, and then can create conjectures, and the put them up for proof to a proof-checking algo/AI?

I don't think we'd still be able to create AIs that would be able to create new forms of mathematics, at least not yet, but surely there must be a way to combine formal statements of patterns in a given constrained domain along with the condition for truth or falseness?

I'm sure more complicated conjectures might not be able to be made at this point, but surely there must be a way for conjectures to be created by machine?
posted by symbioid at 9:21 AM on April 12, 2014

Oh, and speaking as someone who watches things go wrong with software a lot I would be leery of accepting a solution by a computer "using a different approach" as proof. The programmer's intent might be different but it would not surprise me a whit to see the computer end up largely copying the first proof.

If you want to know that things went right you want to forget the content and hammer on the form. We can't understand the overall proof but we should be able to understand each individual step quite clearly.
posted by Tell Me No Lies at 9:21 AM on April 12, 2014 [1 favorite]

Meh. Work is fine, articles overblown. The work here was encoding the conjecture into an instance of the well-studied SAT problem. Solvers for SAT problems have been around...
posted by save alive nothing that breatheth at 9:27 AM on April 12, 2014 [1 favorite]

I've heard that the computer-proof of Fermat's Last Theorem was so long and complicated that no one actually knows if it is correct.
posted by Chocolate Pickle at 10:04 AM on April 12, 2014

There is no computer proof of Fermat's last theorem.
posted by dilaudid at 10:35 AM on April 12, 2014 [2 favorites]

There's also no computer proof -- or any proof, yet -- of the Erdos discrepancy conjecture, despite the linked article incorrectly saying so.
posted by escabeche at 10:53 AM on April 12, 2014

There's also no computer proof -- or any proof, yet -- of the Erdos discrepancy conjecture, despite the linked article incorrectly saying so.

Could you expand on that a bit?
posted by Tell Me No Lies at 11:08 AM on April 12, 2014

The conjecture says that, for every C, every sufficiently long sequence has a subsequence with discrepancy at least C. The new proof shows that this is true for C = 2. They are working on proving it for C = 3 along similar lines. But this is well short of proving it's true for ALL C, which is what the conjecture proposes.
posted by escabeche at 11:24 AM on April 12, 2014 [3 favorites]

C'mon, escabeche, you know that the only important numbers are 0, 1, and ∞. 2 is practically the same thing as ∞.

/L^p-space joke.
posted by benito.strauss at 12:25 PM on April 12, 2014 [5 favorites]

I think the real problem will come not when we can't follow the proof of a conjecture, but when we can't grasp the computer-made conjecture itself.
posted by jamjam at 12:37 PM on April 12, 2014 [1 favorite]

Who computes the computers?
posted by blue_beetle at 1:38 PM on April 12, 2014 [1 favorite]

I read once to bootstrap Lisp someone wrote a minimal Lisp interpreter in Lisp and compiled it to assembly by hand.
posted by save alive nothing that breatheth at 4:06 PM on April 12, 2014

No one really understands the exact circuit layout on the CPU you're using, which was spat out by a similar SAT solver, but it seems to work just fine.

Pesky humans demanding compact forms for boolean equations, harrumph.
posted by RobotVoodooPower at 4:20 PM on April 12, 2014 [2 favorites]

Rather, quis probabit ipsos probatores?
posted by The Tensor at 5:17 PM on April 12, 2014 [4 favorites]

I somehow feel smarter just reading the comments. Please keep it up, you brilliant bastards.

not kidding
posted by nevercalm at 6:29 PM on April 12, 2014 [1 favorite]

No one really understands the exact circuit layout on the CPU you're using, which was spat out by a similar SAT solver, but it seems to work just fine.

Well, unless it's an Intel CPU -- they still do everything by hand. Also, there aren't too many SAT-based synthesis packages used for real problems. Logic synthesis is binate, so minimizing SAT has a bad habit of blowing up for anything larger than a trivially sized circuit. It's useful for automated validation, though.
posted by spiderskull at 11:21 PM on April 12, 2014 [1 favorite]

So I worked in pure maths for quite some time where I did quite a lot of relatively long proof by hand and later I worked on a automated computer proof system with several others, and both approaches to proving things bothered me for different reasons.

For the hand proof, in some sense you never really prove anything. You give a convincing argument that outlines the major logical steps that a proof of the result would have. But you're still writing most of it in English with a bit of mathematical notation, which while much more structured and precise than most any other language, is still not a formal proof. A formal proof uses axioms, formal rules of inference and basically syntactic transforms of symbolic sentences to establish truth. Maybe a few logicians work this way, but 99% of pure mathematicians don't.

The computer proof has the fundamental problem that from a false statement, anything can be proved. So if your automated math prover has a software flaw (who ever heard of code having bugs?) that means that occasionally it can generate the sentence "false" without good reason, perhaps buried very deeply within very large proof, then it'll be able to get any result you like proved.

Neither approach is ideal. But in both cases it's sensible to get someone or something to independently check the working.
posted by drnick at 1:15 AM on April 13, 2014 [2 favorites]

Didn't Douglas Adams already describe how to deal with a computer coming up with an answer beyond our ability to understand?
posted by 1367 at 10:18 AM on April 13, 2014

2 is practically the same thing as ∞.

You say so, but I just came back from a conference where one of the speakers had a good L_2 bound but the L_∞ bound seems totally out of reach, and I'm all, you should do L_4, that's what you do when you can't get an L_∞ bound but you don't want to just give up, and he was all, good point, 4 isn't ∞ but it sure isn't 2. In conclusion, harmonic analysis is a land of contrasts.
posted by escabeche at 6:11 PM on April 13, 2014 [2 favorites]

I knew no good would come from letting COLOSSUS have a data link to GUARDIAN.
posted by radwolf76 at 8:34 AM on April 14, 2014

Well, unless it's an Intel CPU -- they still do everything by hand. Also, there aren't too many SAT-based synthesis packages used for real problems.

I was just going to make a similar comment — but I don't think it's strictly true any more. As I understand it, they currently do the largest scale layout by hand, but many of the portions that go into it are laid out with SAT solvers with constraints to make the results something humans can reasonably stitch together.

Also I seem to recall AMD CPUs and most ARM IP modules are built with automated layout.

Alas, I'm having difficulty finding solid references to back my understanding up.
posted by atbash at 11:21 AM on April 15, 2014

I knew no good would come from letting COLOSSUS have a data link to GUARDIAN.

THERE IS ANOTHER SYSTEM.
posted by kliuless at 8:11 PM on April 15, 2014 [1 favorite]