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.

alexflint 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. Show more comments above.

Comment author: alexflint 16 February 2011 08:58:53PM 0 points [-]

Yes, and the problem of deciding which lemmas to prove and in general what structure to try for a proof is also far from begin formal. Verifying a proposed proof is the formal bit.