``proof assistant''

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

and can come up with ways (algorithms, mnemonics) to get as fast or faster than a computer

Which can then be implemented on a computer. Or the human can still work in tandem with the computer, with part of the algorithm depending on input from the human.