6 ms·
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
by jeapostrophe 13y ago
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.
- freyrs3 13y agoI 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.
- jeapostrophe 13y agoCertainly, but most math proofs aren't "rigorous proofs" by any stretch.