Personally, I'm looking forward to the day when Automated Theorem Provers can compete with top high school students on math competitions. My guess is that the w

Personally, I'm looking forward to the day when Automated Theorem Provers can compete with top high school students on math competitions. My guess is that the way to go is to combine resolution theorem proving with intuitive pattern matching (via deep learning), similar to the way AlphaGo combined monte carlo tree search with deep learning.