[neonhash]

> validate them automatically

That's the hard part. There is some research being done in that are really interesting, such as

* Koepke, Schröder, Cramer with Naproche http://www.naproche.net/index.php

* Paskevich with SAD (unfortunately he stopped his research) https://web.archive.org/web/20131207185950/http://nevidal.or...

[LazerBear]

Maybe I'm missing something, but I don't see the problem. If your users submit their proofs one line at a time, then validating each line is O(1) if they give you the assumptions they used and the steps they took.

Edit: In case I wasn't clear, I didn't mean anything like natural language processing (though that would be awesome). I meant very strict formal math where everything is explicit.