(Replying to PARENT post)
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.
👤LazerBear🕑11y🔼0🗨️0
(Replying to PARENT post)
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...