I’ve always wondered why there isn’t more interest in automated provers. What happens when you make a term-rewriting system with a taste for symmetric, interrelated systems of theorems and have it just search for proofs (and shorter versions of those proofs) for a few years? Do fully artificial mathematicians ever come up with novel theorems? Are they any good at condensing proofs enough that they become comprehensible to humans?
Edit: Had a cursory look through lesswrong history
2015, JoshuaZ: I predict that within 20 years a major conjecture will be made that is essentially found by a computer with no human intervention. Note that this has already happened in some limited contexts for minor math problems. https://cs.uwaterloo.ca/journals/JIS/colton/joisol.html
I’ve always wondered why there isn’t more interest in automated provers. What happens when you make a term-rewriting system with a taste for symmetric, interrelated systems of theorems and have it just search for proofs (and shorter versions of those proofs) for a few years? Do fully artificial mathematicians ever come up with novel theorems? Are they any good at condensing proofs enough that they become comprehensible to humans?
Edit: Had a cursory look through lesswrong history
https://www.lesswrong.com/posts/uu9EAiFwoYg76AAEe/progress-on-automated-mathematical-theorem-proving#hqQJuwRnrESYSomuB
A post by JonahSinick from Jul 2013, asking the very question Progress on automated mathematical theorem proving?
https://www.lesswrong.com/posts/w9Wx3PXSCfZFCGxff/discussion-of-concrete-near-to-middle-term-trends-in-ai#ArmbHFn62E24HRShs
https://www.lesswrong.com/posts/uu9EAiFwoYg76AAEe/progress-on-automated-mathematical-theorem-proving#hqQJuwRnrESYSomuB
The competition still seems to be active. Last year’s winners were Satallax 3.3, Vampire 4.3 (in three categories), iProver 2.8, and MaLARea 0.6