``proof assistant''

Gödel didn't need a proof assistant, why do you? You'll never succeed in making maths entirely computable, automatable, never.

Automatic theorem solving is even bigger crackpottery than "Strong AI", because even human brain gives no guarantees in seeing immediate solution to something as simple as Pythagoras' Theorem, which was proven only when substantial practical basis was accumulated, allowing to make a guess that there is a law, allowing breaking stuff into vectors, so the theory wasn't finalized till Descartes. This leads me to think that mathematics isn't a thing in itself, but heavily depends on physical observations and statistics.