``proof assistant''

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

>>8

the realm of computationally possible things is pretty big.

Fortunately, [b]P ≠ NP[/b], so no, not really.

Where's the computer that ``verified'' Wiles' proof of Fermat's Last Theorem? Oh wait,

A computer science challenge given in 2005 is "Formalize and verify by computer a proof of Fermat's Last Theorem, as proved by A. Wiles in 1995."[30]

LOL!