> The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for

> The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error. Rather than “redundancy”, it's a matter of having nice (algebraic, geometric, whatever) structure. Of course, a pure mathematician has more freedom than a programmer to decide what kinds of structures he wants to work with. > statements that are rather trivial and obvious, but very subtle in the edge cases. This is a contradiction in terms. If it seems “trivial and obvious”, but is actually “subtle in the edge cases”, then you are underestimating its complexity. > Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons. Then you need to roll up your sleeves and actually prove things, not just skim through purported proofs.