> It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. What about things like Metamath [1]? (Not sure if

> It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. What about things like Metamath [1]? (Not sure if there is a more mature similar effort, Metamath is just the one I've heard of.) It seems like it has quite a lot of the "thousand other trivialiaties" you mentioned, but maybe it's still not enough to make a real dent? [1] http://us.metamath.org/index.html http://us.metamath.org/index.html