Hmm, yeah, you are right. Rybka, Deep Fritz and their predecessors look like a smaller effort than ATPs, actually. And other chess programs are at about the same level (and close to the top human players' level, apparently?). Both areas look from outside like good targets for narrow AI , but apparently there is something about theorem proving that requires some poorly formalized part of human reasoning.
Human chess also involves loads of poorly formalized reasoning, but chess is a vastly smaller search space. There is no game you can play which gets you to Fermat's Last Theorem.
Ganesalingam and Gowers recently released an ArXiV preprint of their article "A fully automatic problem solver with human-style output" about a theorem-proving program they have written that generates human-readable output. Gowers had blogged about the program in April 2013, after soliciting responses from readers regarding answers generated by the program and by humans (without explicitly revealing that one of the answerers was a machine) in March 2013.
There do exist theorem-proving systems such as Coq. In fact, it was announced about a year ago that the proof of the Feit-Thompson odd-order theorem, which originally appeared in a 255-page journal article in 1963, had been completely verified using Coq. But the Gowers-Ganesalingam program differs in that the output of this program is a human-style proof (for better or worse) whereas Coq uses a formal language syntax (see here for a small part of the proof of the Feit-Thompson theorem using Coq).
The ArXiV preprint contains details of the program and how the authors believe it improves on existing programs. One of the ways they believe they are better than past provers is their ability to more explicitly code for picking promising lines of reasoning.
I'd appreciate comments from LessWrong readers about the specifics of the Ganesalingam-Gowers program, and any broader ramifications of their ability to create this program for predictions related to artificial intelligence.