You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

timtyler comments on Automated theorem proving by learning from examples - Less Wrong Discussion

3 Post author: alexflint 16 February 2011 01:38PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (9)

You are viewing a single comment's thread.

Comment author: timtyler 16 February 2011 01:57:20PM 2 points [-]

Most theorems are not presented in a very machine-friendly format, I believe.

Comment author: alexflint 16 February 2011 08:52:51PM 1 point [-]

Yes but parsing theorems (at least at the syntactic level) should be no harder than parsing English, and we do lots of reasonably smart text mining, and even some reasonable natural language translation.

Comment author: timtyler 16 February 2011 09:10:59PM *  1 point [-]

Math theorems are hard-going for many humans. Machines think differently - but may well find them challenging too. I'm not sure this area is particularly low-hanging.