Computers beat humans at Computation, Enumeration and even (though most people don’t realise this) Deduction. However, a central feature of most mathematics is relating to the literature, which in practise is gathering together results (and concepts) to be used for deduction. However, computers at present do not search the (human) literature. In the hope of eventually teaching them, here are the steps by which I proved a lemma.
The lemma is a statement of the following nature.
Lemma: For words a, b, A and B in the fundamental group of a surface satisfying some conditions, if ab=AB then a=A and b=B.
Here are the steps in my discovery of a proof:
- The starting point was a result of Chas-Krongold, which was a special case in a more restricted context, plus knowing from Moira Chas that she had proved (but not published) a result similar to my lemma but in a more restricted context.
- The Chas-Krongold work used what is called small cancellation theory. It is well known that a method that proves the same results in more generality (at the cost of weaker estimates) is $\latex\delta$-hyperbolicity, which is applicable in our context.
- To use word-hyperbolicity, I tried to construct quasi-geodesics associated to ab and AB. This is what we can try to associate to elements.
- The construction of the quasi-geodesics was the most obvious one. The issue was to prove it was a quasi-geodesic. Here I used a non-trivial theorem – local quasi-geodesics are quasi-geodesics.
- To verify that what we obtained was a local quasi-geodesic, one used some geometry and another lemma – a lower bound on angles.
- To get the lower bound on angles involved using another known trick from the literature – consider the commutator and show that it is small.
- Now that we have quasi-geodesics, we use one of the main theorems concerning $\latex\delta$-hyperbolicity, that quasi-geodesics are close to geodesics.
- Now we use some geometry parallel to the combinatorics of Chas-Krongold and the trick of considering commutators to finish the proof.
The deductions are not difficult at any point. The main obstacle to automation (say of a computer as a collaborator) is to be able to make the right analogies and dig up the literature. Indeed the analogy is also not that obscure – early papers on $\latex\delta$-hyperbolicity do show that the results include those of small-cancellation theory.
The main barrier is understanding natural language. In the sequel I speculate on a scheme to try this.