5 ms·
> 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
by 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.