As with many other real-world distributions, the class of open problems in mathematics has a "long tail" - a large number of problems which would be relatively easy to prove or disprove, but which have not recieved significant attention from the (limited) number of expert mathematicians available. To switch metaphors, this tail can thus contain a large amount of "low-hanging fruit" of new mathematical results that could be obtained if there was some way to automatically attack these problems at scale.

I saw this first-hand when running the Equational Theories Project last year, in which 22 million implications in universal algebra were attacked (and ultimately resolved). Initial passes with low-tech automated methods resolved a large percentage of these implications within days, with increasingly sophisticated methods brought to bear to pick off the more stubborn holdouts that resisted earlier sweeps. The final few implications took months of human effort to settle: https://github.com/teorth/equational_theories/wiki/Terence-Tao's-personal-log

(1/3)