That problem was solved by a non learning AI system decades ago. Current theorem provers (a related field of AI) solve problems like this in fractions of a second.
The progress in the article is getting a learning system to do so, eventually leading us to handle unsolved problems.
This seems like a bit of an unfair comparison. The 'decades ago' solution was a system, built by humans, that can solve this problem (and very closely related ones), whereas this solution is a system, built by humans, that can design a system to solve the problem.
I agree with the point taniq makes in that those easier systems did in fact require a lot of hand crafting, even if parts were automated. I find it interesting the points at which the usefulness of these approaches plateaus.
I am interested a lot in general game playing, and there is a common problem that while the general systems tend to make interesting progress, it is the systems finely crafted to the game that win competitions.
What I am really, REALLY interested in is what commercial application exist for these types of technologies. Solving a puzzle slightly better than a different tool is fun, but solving a valuable business problem is where the money is at.
No, it is not an unfair comparison. Those systems were not hand crafted. They were implemented via first-order logic theorem provers. FOL theorem proving is Turing complete and extremely expressive.
This not a me vs you camp. Just a scientific statement.
The progress in the article is getting a learning system to do so, eventually leading us to handle unsolved problems.