JonahSinick comments on Progress on automated mathematical theorem proving? - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (65)
Given that I think that capturing the ingenuity of human mathematicians is one of the last things I'd expect to see before seeing human-level-or-smarter AI, the poor state of automated theorem proving doesn't seem to me like much evidence on how far away GAI might be.
Also note that the Sylow theorems are, in some sense, a pretty low bar. Compare with the Feit-Thompson Theorem, which has a proof running 250 pages, and which builds on previously known results. I have a friend who's a finite group theorist who said that in many cases he struggled to verify the truth of individual lines of the proof.