Progress on automated mathematical theorem proving?

In a re­cent com­ment thread I ex­pressed skep­ti­cism as to whether there’s been mean­ingful progress on gen­eral ar­tifi­cial in­tel­li­gence.

I hedged be­cause of my lack of sub­ject mat­ter knowl­edge, but think­ing it over, I re­al­ized that I do have rele­vant sub­ject mat­ter knowl­edge, com­ing from my back­ground in pure math.

In a blog post from April 2013, Fields Medal­ist Ti­mothy Gow­ers wrote:

Over the last three years, I have been col­lab­o­rat­ing with Mo­han Gane­sal­ingam, a com­puter sci­en­tist, lin­guist and math­e­mat­i­cian (and amaz­ingly good at all three) on a pro­ject to write pro­grams that can solve math­e­mat­i­cal prob­lems. We have re­cently pro­duced our first pro­gram. It is rather rudi­men­tary: the only prob­lems it can solve are ones that math­e­mat­i­ci­ans would de­scribe as very rou­tine and not re­quiring any ideas, and even within that class of prob­lems there are con­sid­er­able re­stric­tions on what it can do; we plan to write more so­phis­ti­cated pro­grams in the fu­ture.

I don’t know of any com­puter pro­grams that have been able to prove the­o­rems out­side of the class “very rou­tine and not re­quiring any ideas,” with­out hu­man as­sis­tance (and with­out be­ing heav­ily spe­cial­ized to an in­di­vi­d­ual the­o­rem). I think that if such pro­jects ex­isted, Gow­ers would be aware of them and would likely have com­mented on them within his post.

It’s easy to give an al­gorithm that gen­er­ates a proof of a math­e­mat­i­cal the­o­rem that’s prov­able: choose a for­mal lan­guage with defi­ni­tions and ax­ioms, and for suc­ces­sive val­ues of n, enu­mer­ate all se­quences of math­e­mat­i­cal de­duc­tions of length n, halt­ing if the fi­nal line of a se­quence is the state­ment of the the de­sired the­o­rem. But the run­ning time of this al­gorithm is ex­po­nen­tial in the length of the proof, and the al­gorithm is in­fea­si­ble to im­ple­ment ex­cept for the­o­rems with very short proofs.

It ap­pears that the situ­a­tion is not “there are com­puter pro­grams that are able to prove math­e­mat­i­cal the­o­rems, just not as yet as effi­ciently as hu­mans,” but rather “com­puter pro­grams are un­able to prove any non­triv­ial the­o­rems.”

I’ll high­light the Sy­low the­o­rems from group the­ory as ex­am­ples of non­triv­ial the­o­rems. Their state­ments are sim­ple, and their proofs are not very long, but they’re in­ge­nious, and in­volve sub­stan­tive ideas. If some­body was able to write a pro­gram that’s able to find proofs of the Sy­low the­o­rems, I would con­sider that to be strong ev­i­dence that there’s been mean­ingful progress on gen­eral ar­tifi­cial in­tel­li­gence. In ab­sence of such ex­am­ples, I have a strong prior against there hav­ing been mean­ingful progress on gen­eral ar­tifi­cial in­tel­li­gence.

I will up­date my views if I learn of the ex­is­tence of such pro­grams, or of pro­grams that are ca­pa­ble of com­pa­rably im­pres­sive origi­nal re­search in do­mains out­side of math.