# Why is it hard to formalize informal proofs?

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.

• I think this question should be clearer. The second paragraph seems to confuse "impossible" with "possible but really hard".
– Trebor
Jan 13 at 13:59

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.

• Note that the word problem in a monoid is semidecidable. So there is an algorithm that will terminate on any true equation, but won't necessarily terminate on false equations. Jan 28 at 20:16
• Cool! I thought it was undecidable, like for groups. Do you have a reference to the semi-algorithm? Jan 31 at 9:59
• The semidecision procedure works for groups as well. It's not a fast procedure. Basically, two terms are equal according to a set of rules if they is some finite sequence of rewrites proving they are equal. There are only countably many finite sequences of rewrites, so by enumerating them and trying each of them you will eventually find the correct one if it exists. If such a sequence of rewrites does not exists, the search goes on forever. Jan 31 at 11:30