ideally it will be faster than doing it by hand That's a good point... I agree the tools are not ready. Most computer-assisted tools make it easier to do your

ideally it will be faster than doing it by hand That's a good point... I agree the tools are not ready. Most computer-assisted tools make it easier to do your work. It's easier to type a five page paper in Word than it is to write it longhand. But for now it's a lot more work to encode a proof in a proof assistant than to just write it up in LaTeX (which I think a lot of people don't realize). It's not just that the foundational concepts are missing, it's also that proof assistants currently require you to fill in much more detail than human proofs do. You can't just write something like... "this corollary is trivial", or, "since x is a power of 10, obviously cos(x^2) is irrational"; you have to spell out a proof.