Hacker News new | ask | show | jobs
by freyrs3 4687 days ago
> 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."

1 comments

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.