cousin_it comments on Automated theorem proving by learning from examples

[cousin_it]

Again I’ll have to agree with timtyler. Formalizing mathematical proofs is difficult, see my old post. Maybe you’ll find it easiest to use an existing corpus, like Metamath.

[Alex Flint]

Ooh, thanks for the link to metamath.