``proof assistant''

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

>>5
The computer has an inferior verification rate and ability compared to the human. Computers are only good for arithmetic and that's only because arithmetic is boring and anybody can do it.