For every theory, define its axioms and valid logical steps. Let anyone build theorems based on these (validate them automatically), and allow people to fork others theorems to create their own.
It's probably possible to get a lot of proofs from projects like Mizar and Metamath to start with, then let the community build on top of it.
Maybe even a crowd sourced bounty program for unproven theorems, like P=NP. Let people pledge and automatically pay to whoever proves or disproves it.
I think this can really change how mathematical research is done.
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.
For every theory, define its axioms and valid logical steps. Let anyone build theorems based on these (validate them automatically), and allow people to fork others theorems to create their own.
It's probably possible to get a lot of proofs from projects like Mizar and Metamath to start with, then let the community build on top of it.
Maybe even a crowd sourced bounty program for unproven theorems, like P=NP. Let people pledge and automatically pay to whoever proves or disproves it.
I think this can really change how mathematical research is done.