[brzozowski]

> Computers will never fully automate mathematical reasoning, because mathematical reasoning cannot be fully automated.

One possible reason why mathematics cannot be automated is because some important piece of contemporary mathematics is fundamentally unsound, e.g. ∞, LEM, AOC. Mathematicians are very clever at building and manipulating formal systems, but are prone to mistakes and must accept on faith some foundations to make any progress. If you spent your entire career building a castle and someone like Gödel or Brouwer came along and claimed the whole thing is built on sand, naturally you (and all your venerable castle-building colleagues) would be unwilling to simply accept this development and move on.

I suspect what many people call mathematics today lost its course somewhere after Cantor, who was a supremely clever human being, but either mentally unstable or driven to madness trying to operationalize infinite sets. If our universe were infinite, maybe his ideas would be valid, but even then we could never build machines to verify those claims. While it has produced an abundance of useful ideas, it also generates a number of paradoxes (e.g. Zeno, Banach-Tarski), which are simply incompatible with the universe in which we live.

[kd0amg]

Unsound with respect to what?

[sukilot]

It's hard to say that human math is unsound when it's not even well defined. Human math sits on a substantial foundation of faith, and always will.