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.