Speaker: Richard Parker (Cambridge)
Title: On Short Theorems with a Long Proof
Abstract:
Given a presentation of a group, coset enumeration and various kinds of Knuth-Bendix can be used to try to investigate it. They all tend to fail if there is a "Short Theorem with a Long Proof" (STLP).
An alternative idea is to look directly for STLPs, defining "Short theorem" in terms of word length and "Long Proof" as a large minimal number of conjugates of relators that must be multiplied and cancelled to make it.
Fitting relators together is a bit like building polyhedra (via van Kampen diagrams) and the concept of "curvature" can be used to guide the search.
The principles seem clear, yet turning them into an actual algorithm seems to be a heroic struggle.