``proof assistant''

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

I'd like to have a system where anyone can submit a proof that is automatically verified by the computer, and, if correct, is added to a database which anyone can browse.