5 ms·
GitHub for mathematicians. For every theory, define its axioms and valid logical steps. Let anyone build theorems based on these (validate them automatically),
by LazerBear 12y ago
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.
- ninguem2 12y agoOne day, perhaps. Automatic checking of proofs is nowhere near there yet for most serious mathematics.
- neonhash 12y ago> 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 http://www.naproche.net/index.php * Paskevich with SAD (unfortunately he stopped his research) https://web.archive.org/web/20131207185950/http://nevidal.org/sad.en.html https://web.archive.org/web/20131207185950/http://nevidal.or...
- LazerBear 12y agoMaybe 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.