Hacker News Reader

Comment by jeapostrophe | Hacker News Reader

We should not throw out mathematics, but we should recognize that most mathematical proofs are not based on logic, but human intuition in the first place. Human intuition and wisdom are valuable and lay the foundation for all that we do and there's no reason to ignore them when we're programming and insist that all valid programs have to follow some particular set of rules.

View on HN

> mathematical proofs are not based on logic

Mathematical proofs are explicitly logical statements, if they aren't based in logic they aren't proofs by definition. Mathematical intuition is what leads us to ideas but it's only within the framework of formal reasoning that we "know" anything within mathematics. Poincare said it nicely:

"It is by logic we prove, it is by intuition that we invent."

If you really believe this, you should try to translate any contemporary (published) mathematical proof into a real logic, like Coq. It is hard and people earn PhDs doing this because most proofs are so intuition heavy in the first place.

I have spent several months doing proofs in Coq, as well as in Isabelle. I contest conflating Coq with "real logic", it is perfectly possible to do rigorous proofs without the aid of a computer-aided proof assistant, if that wasn't the case then there wouldn't be any reason to trust the authors of the proof assistant in the first place.

Certainly, but most math proofs aren't "rigorous proofs" by any stretch.

Reply on news.ycombinator.com