[Koshkin]

> The future is mechanical proofs.

That almost sounds like "the future is mechanically composed novels" (or music). Understanding why something is true is just as important as knowing that it is. Mechanical proofs will be impossible for humans to understand, so the value of such proofs will be rather limited (in that people will still continue searching for a "real" proof).

[pacala]

Mechanical proofs and understanding are not mutually exclusive, that's the whole point! Just like mechanical processes [aka software] are still understandable. A stronger conjecture is that mechanical proofs will enable _better_ understanding, as tools and metrics are developed for tackling "understanding".

[hilbertseries]

Have you ever read a mechanical proof or studied mathematics at the graduate level? It's incredible difficult to prove even basic things in the current mathematical proof dialectics and reading the proofs is even more painful. Maybe there will a come a time when mathematical proofs are helpful, but it's not a particularly active area of research and the amount of work to be done in it is monumental in order to get to the point you're proposing.

[pacala]

I stole a small part of http://compcert.inria.fr for a hobby project. While this is not "graduate level mathematics", it is "graduate level computer science". I could have never done it if I had to memorize half a book of definitions just to warm up.