Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

It's because a good proof conveys human-level insight first and foremost, and the details are often mental baggage that can be sorted out later.

Proof assistants are the opposite. Sacrifice intuition and insight for the sake of correctness.

This is also why mathematicians love picture proofs.



I am not satisfied by picture proofs, I'd like to see derivations from axioms and known results.

I love pictures that give me intuition about a proof and I agree that intuition is crucial to understanding. But all the intuition in the world is useless if the proof fails because of one tiny logically unsound step or one pathological corner case, so it's no good to ignore the technical details or, even worse, to become unable to expand a purpoted proof one has written into a fully detailed version, which I suppose can easily happen if someone relies too much on intuition.


Of course you can't ignore details. I was explaining the source of emotions, which tend to drive whether one wants to adopt a particular tool or method.

That being said, I often find convincing, false proofs as illuminating as true proofs, once the flaw is clear, because they highlight the nature of the conjecture. So I disagree with your claim that a proof can suddenly become useless due to a slight misstep.

And for what it's worth, theorems are rarely thrown out due to pathological corner cases; at least I've never heard of this happening. Instead, if the insight conveyed by the proof is useful, it's called a partial result and the conditions are modified to fit the proof. Entire theories are built up specifically to avoid pathology (almost every mathematical field does this)




Consider applying for YC's Summer 2026 batch! Applications are open till May 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: