[patmcguire]

Sort of like the Four Color Theorem, in that it's something that was proven with computers and brute force. I remembering hearing mathemeticians were upset about it because it just felt wrong to prove it that way (this was the 70s, it may have been the first proof that was done by machine) http://en.wikipedia.org/wiki/Four_color_theorem

[sharkweek]

My math teacher in high school (this was before Wikipedia) told our calculus class at the beginning of the year if we could prove how to only use four colors on a map without any similar colors touching, he'd give us a 4.0 for the class.

Years later and long after I had forgotten most of the math I learned, I saw the four color theorem on Wikipedia and got such a kick out of the absurdity of my teacher's offer.

Brought it up with him when I randomly bumped into him a little bit ago, he got quite a kick out of it.

[Pitarou]

That's right, The Four Color Theorem was the first such proof.

Mathematicians weren't so much "upset" as "not sure what to make of it". Technically, the "proof" wasn't really a proof at all, because it relied on the operation of a computer program, and the compiler / OS / hardware stack upon which the program operated had not been rigorously verified.

Even if it HAD been verified, there's still the question of whether transistors always work in the way we believe....

Of course, over the years, the Four Color Theorem has been checked 100s of times, with many different software / hardware stacks. But to a purist, this still only counts as "strong evidence" rather than "proof".

[lincolnq]

It's weird to say that and still count written proofs. There's still the question of whether neurons always work in the way we believe...

[Pitarou]

Shh! Don't tell them that. You'll hurt their feelings.

[eli_gottlieb]

I genuinely find it hard to believe mathematicians could function professionally as mind-body dualists, especially given how many major mathematicians are non-neurotypical.

[infruset]

>this still only counts as "strong evidence" rather than "proof".

Please allow me to disagree. Georges Gonthier proved the Four Color theorem using the proof assistant Coq, which is as much of a certainty as you're ever likely to get for a mathematical proof. http://www.ams.org/notices/200811/tx081101382p.pdf

[lurkinggrue]

I suppose you could just forge your own silicon and software and submit that as part of the proof.

[Pitarou]

No. That wouldn't be sufficient. Here's why.

Imagine that I built a machine and told you, "Press this button here. If P=NP, the lamp will turn on. If P!=NP, the lamp will not turn on." What would you make of it?

So what if I opened up the machine, and showed you all the components, would that convince you?

I think you'd only be convinced, if:

1. We could agree on some basic axioms of how the basic components of the machine operates.

2. From those axioms, I could prove the proposition that, for a machine of this design, the lamp will turn on if and only if P=NP.

I think that, one day, somebody WILL construct a formally verified silicon system capable of proving the four color theorem. (Putting aside the issue of unreliable logic gates.) But I don't think it will be in some high-level system like Coq, because there are so many layers of abstraction we would have to formally verify. I think it's more likely that the logic would be implemented directly in silicon.

[lifeformed]

It's still a proof, just an inelegant one. But I agree, it's considerably different than standard proofs, since it doesn't explain "why".