Why is it hard to formalize informal proofs?

Question

Say I have some informal but rigorous argument in line with eg real analysis. Currently, it is a massive PITA to do algebraic manipulations in proof assistants like Coq or Isabelle. However, in informal proofs we can "just" prove commutativity, associativity, etc, then do some hand-waving and say "we can always go back to axioms if needed".

Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc? If it really is possible to "always go back to axioms" then it should be implementable on a computer, right? If that's not possible, we can reliably verify informal arguments with our brains, so we should be able to realize whatever algorithm our brains use mechanically.

Answer 1

Are there any theoretical obstacles in formalizing what we actually do when we mentally verify equations, etc?

Yes: we don't know what we actually do when we mentally verify equations!

This is a glib answer, but it is actually correct for deep reasons. Many of the natural or obvious formalisations of what people do turn out to be undecidable.

For example, consider a presentation of a monoid via a set of generators (e.g., $\{a, b, c, d\}$) and a set of equations (e.g., $a\cdot b \cdot c = c \cdot c$) between words. You can use these equations plus the axioms for monoids to prove equations like $a\cdot b\cdot a\cdot b\cdot c = c\cdot c\cdot c$.

However, the general word problem (I'll give you a set of generators and equations, and you decide whether an equation holds or not) is undecidable.

Therefore, humans must be doing something simpler than that. But we don't know what that is, specifically, and the algorithms our computers use can do some things much more powerfully than any human can (eg, Vampire or Z3 can automatically prove truly amazing things), but are also often give much worse results than what humans can do.