= 27d567bc2d48d9f40e9ccc20ea370b15)
Vladimir_Nesov comments on Automated theorem proving by learning from examples - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (9)
The problem of deciding which definitions are interesting is far from being formal.
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.