Thoughts on automated reasoning

I strongly disagree that proofs done by computers are less trustworthy than those done by humans. I also disagree that creative mathematics is not amenable to mechanization. Human brains are a narrow set of algorithms. We have bias and limitations that force us to look at a specific set of functions and properties in extreme detail. We know a lot about polynomials and Euclidean space for instance, yet our working memory is limited, and so complicated objects, where many parts need to be considered at once, are impossible for most of us to study. The search space of any reasonably expressive system is so vast that if computers are to compete with humans, we must prune the space substantially. In some way, we must relay what constitutes interesting mathematics.

It may be difficult to formalize a predicate of interesting mathematics, but there are common themes. For example, humans are wildly interested in symmetry. Is that because bilateral symmetry is a sign of good health? We also love short formulas, like \(E = mc^2\) and \(e^{i\pi} = -1.\) If some theorem is interesting in some number of dimensions, then it's generalization to \(n\)-dimensions is likely interesting as well. Characterizations are interesting, such as the characterization of Eulerian graphs. If a shape is interesting, then almost surely its area and perimeter formulas are interesting as well. Humans are also interested in visual proofs of interesting formulas. Correspondences are often interesting, such as the Curry-Howard correspondence. My guess is that you could take a computer, run it over all the textbooks available, and get a good idea of what constitutes interesting mathematics. Sure, this picture would be incomplete, but it may be useful to set computers on a guided search for interesting math, in the same way an artificial intelligence program might learn how to write newspaper articles or paint.