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.
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.