Nov 07, 2016

Check out the "Deepmath" paper linked above. (The paper is from a few months ago, the source code is new IIUC.)

https://arxiv.org/abs/1606.04442

Jul 15, 2016

It seems kind of strange that he never thought of using computer proof systems for checking whether his proofs were right in class, and that he took a pattern-matching approach rather than using any of the existing AI proof-deriving systems like https://arxiv.org/abs/1606.04442 or https://intelligence.org/2013/12/21/josef-urban-on-machine-l...