undefined | Better HN

0 pointshyperbovine1y ago0 comments

What if the proof were incomprehensible to humans?

0 comments

If it cannot explain how it was proven, was it actually proven?

No. Funny how these discussions too often devolve into semantics lol.

Funny how people don't understand basic logic. If it is a proof in a logic, and the machine checked that proof, it is a proof, no matter that no human actually understands it.

A human doesn't need to understand the proof, they just have to understand why the proof is a proof.

3 more replies

fennecfoxy1y ago

If it cannot explain to a human*

Yes, it was still proven. If I don't speak English but come up with a proof, I can't communicate the proof, but I have still proven (ie created proof) it.

humansareok11y ago

If we can formally verify the proof then it doesn't matter. Often the implications on other problems is substantial just knowing the proof exists.

camjw1y ago

I think that is unlikely to be the case - the classic example of a proof that human's "can't understand" is the Four Colour Theorem, but thats because the proof is a reduction to like 100000 special cases which are checked by computer.

To what extent is the proof of Fermat's Last Theorem "incomprehensible to humans" because only like a dozen people on the planet could truly understand it - I don't know.

The point of new proofs is really to learn new things about mathematics, and I'm sure we would learn something from a proof of Goldbach's conjecture.

Finally if it's not peer reviewed then its not a real proof eh.

hyperbovineOP1y ago

I think the 4-color theorem is rather different though. It reduced to a large number of cases that can in principle each be verified by a human, if they were so inclined (indeed a few intrepid mathematicians have done so over the years, at least partially.) The point of using a computer was to reduce drudgery, not to prove highly non-obvious things.

Thinking back to Wiles' proof of FLT, it took the community several years of intense work just to verify/converge on the correct result. And that proof is ~130 pages.

So, what if the computer produced a provably correct, 4000-page proof of the Goldbach conjecture?

steego1y ago

It shouldn’t count. We need to require it be able to ELI5 the proof to Goldbach’s conjecture to an actual class of graduating kindergartners.

j / k navigate · click thread line to collapse