Hacker News Reader

Comment by hyperbovine | Hacker News Reader

What if the proof were incomprehensible to humans?

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.

The useful thing about proofs is that they are written in English (or another language), not formal logic. In general they can be mapped to formal logic, though. This means that people can digest them on an intuitive level. The actual goal of a proof is to create new knowledge (via the proof) which can be distributed across the mathematical community. If proofs exist but are not easily comprehensible, then they don’t accomplish this goal.

If a proof is understandable only by a few people in the world, I would say it fails as a proof, according to your definition. There are many such proofs out there right now. It doesn't help that many of them are wrong, albeit usually in a fixable way.

Making a proof formal doesn't mean it is not understandable any more. First, certainly a machine can "understand" it now. I think with AI improving what exactly such an understanding is worth, and what you can do with it, will increase a lot.

Secondly, the inscrutable tactics-based proofs featured in Lean (I have written such proofs in Isabelle in 1996) are actually quite old-fashioned for such a "modern" prover. Isabelle has long featured human-friendly syntax, and these proofs are certainly as understandable as English text, if written with care.

What we will soon get are proof assistants which allow you to write your proofs (and definitions) in English, but which are still fully formal and checkable. That is an immense help if you are producing new knowledge, because usually nobody else looks at your work with sufficient scrutiny in the first place. If you understand it, and in addition the machine "understands" it, I think that will be the gold standard for proofs very soon.

It will also help mathematicians to clean up their act ;-)

Well... assuming a human made no mistakes setting up that logic.

Of course. That falls under "understanding why the proof is a proof".

Now we only need to find that human that never makes mistakes and we're golden...

Luckily, that is not necessary. You can make many mistakes, until you arrive at a logic you are happy with. Then you talk with other humans about it, and eventually you will all agree, that to the best of your knowledge, there is no mistake in the logic. If you pick first-order logic, that has already been done for you.

Then you need to implement that logic in software, and again, you can and will mistakes here. You will use the first version of that software, or another logic software, to verify that your informal thoughts why your logic implementation is correct, can be formalised and checked. You will find mistakes, and fix them, and check that your correctness proof still goes through. It is very unlikely that it won't, but if it doesn't, you fix your correctness proof. If you can indeed fix it, you are done, no mistakes remain. If you cannot, something must be wrong with your implementation, so rinse and repeat.

At the end of this, you have a logic, and a logic implementation, which doesn't contain any mistakes. Guaranteed.

We just have different definitions of what a proof is. Hence, semantics.

I would rather say that I actually have a definition of what a proof is, and you don't. But feel free to prove me wrong (pun intended), and tell me yours.

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.

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.

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.

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?

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.

Reply on news.ycombinator.com