[LazerBear]

GitHub for mathematicians.

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.

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

[ninguem2]

One day, perhaps. Automatic checking of proofs is nowhere near there yet for most serious mathematics.