6 Concluding remarks

The end of the previous section suggests a fairly radical proof strategy: swap out the torus \(\mathcal{S}\) for a different triangulated surface and see what you prove. Well, once again Richter-Gebert rose to the occasion and developed these ideas into a computable algorithm (Richter-Gebert 2006). In truth, to get a truly impressive proof strategy you need to flesh out the material we’ve covered a bit more. In particular, you need to be able to equip the triangles in your triangulation, not just with the Pappus configuration, but also with the Menelaus configuration (which has its own associated theorem). From now on we shall use the term TS proof (Triangulated Surface) to denote a proof that uses this strategy. TS proofs have been around for a little while now; the earliest example I know of appears on page 68 in Coxeter and Greitzer (1967).

To conclude this essay we explore aspects of the TS proof system in the style of the papers Richter-Gebert (2006) and Apel and Richter-Gebert (2010): individually addressing a list of questions and topics.

  • What happens if we glue our geometric configurations around a different triangulated surface? The answer to this question is exactly what one would hope for: you prove loads of different theorems. The wonderful fact is that the TS proof strategy isn’t just elegant, it’s also really powerful. Remember back in Section 3 where we discussed binomial proofs? Well, it turns out that there’s a deep connection between that proof strategy and the TS proof strategy. It’s been shown that any theorem which admits a binomial proof also admits a TS proof (Apel and Richter-Gebert 2010). This includes many well-knows results: Miguel’s theorem, Desargues’ theorem and Thales’ theorem to name a few. For an impressive collection of such results, see Crapo and Richter-Gebert (1995).

  • The proof landscape. My favourite aspect of the TS proof strategy is the perspective it gives on the landscape of all projective incidence proofs. Sure, binomial proofs already gave us a systematic way of exploring that landscape, but the TS proof strategy gives us one that’s so much richer. Exploring the landscape via binomial proofs essentially labels a proof by its hypotheses and conclusion – pretty standard stuff. Exploring with the TS proof strategy labels a proof by a triangulated surface (!) and assignment of either Ceva or Menelaus to each triangle. So many interesting questions fall out of this perspective. What happens if we glue two proofs together by gluing their triangulated surfaces together?10 Is there a connection between Pappus being the simplest non-trivial binomial theorem and the torus being the simplest topologically non-trivial surface? And finally, leading to our next question, can we really assign a shape to a theorem?

  • Is there really such a thing as the shape of a theorem? This question is explicitly addressed by Apel and Richter-Gebert (2010). We reproduce their answer here:

    The manifold proofs [i.e. the TS proofs] come along with a natural topology. In particular we have seen two proofs of Pappus’s theorem and both beared the structure of a torus. Is the topological type of the proof an invariant of the theorem? So far we were not able to find Ceva-Menelaus proofs for Pappus’s theorem that had a different topological type (as long as we exclude the possibility of adding additional generic points).

    It sounds like we have evidence for the answer being yes, but the question remains open.11 This does mean that titling this essay The shape of a theorem was a bit tenuous… if any projective geometers are reading, please work on settling this question (preferably in the affirmative).

  • Sure, TS proofs have a certain elegance to them, but we already had binomial proofs and they seem simpler. If you agree with this sentiment, that might be partly due to my biases and how they come across in this account. I really wanted to include binomial proofs to illustrate the power of TS proofs, but I didn’t want them to become the focus. For this reason, I presented binomial proofs in as economical a fashion as I could, whereas I drew out every single detail of the TS proof of Pappus’ theorem.12 This could give readers the impression that binomial proofs are simpler than they really are. In particular, we didn’t even attempt to cover the Grassmann–Plücker relations and not proving Proposition B sweeps a lot (i.e. projective transformations) under the rug. Let’s put it this way: if you’d kidnapped me just after finishing my BSc in maths, isolated me on an island and told me that I couldn’t leave until I’d proved Pappus’ theorem, I think it would be more likely that I’d stumble into the TS-proof rather than reinvent the foundations of projective geometry and provide a binomial proof.13

    A potential reason to prefer TS proofs is that they tend to provide more satisfying explanations. If one interrogates the binomial proof of Pappus’ theorem as to why the result holds, it can feel like the only answer provided is because the linear algebra says so. On the other hand, the TS proof responds with because you can equip this triangulated torus with compatible Ceva configurations. Whether or not the second answer is more enlightening is probably up for debate, but it is certainly more expressive.

  • Where did all the projective geometry go? This is a fair question: we spent a lot of time setting up projective geometry at the beginning, but then, as the essay progressed, it just sort of fell away. I did toy with the idea of removing any mention of projective geometry (which would’ve also allowed me to cut a certain amount of set-up). However, as previously mentioned, including binomial proofs felt important to sell the power of TS proofs, and you can’t even discuss binomial proofs without homogeneous coordinates. So I bit the bullet and wrote Section 2. On reflection, I think it turned out well. I like how simplifying the statement of Pappus’ theorem works as an initial motivation for introducing the projective framework.

    The fact that we didn’t need to refer back to projective ideas when developing our TS proof of Pappus’ theorem highlights an interesting aspect of TS proofs more generally. The proof strategy is essentially agnostic as to whether the configurations one attaches to the triangles are projective or Euclidean. In other words, whether the TS-proof strategy produces Euclidean or projective results comes down to whether we think of the corresponding Ceva and Menelaus configurations as Euclidean or projective. This seems different to the binomial proof strategy which, as far as I know, doesn’t have a Euclidean counterpart.

  1. An example of this is explored in Section 7 of Richter-Gebert (2006)↩︎

  2. I’m sure we all agree this is the most exciting possibility.↩︎

  3. Seriously, in most references the entirety of Section 5 is condensed into a few sentences.↩︎

  4. Of course, it’s far more likely that I’d die of old age before finding either proof.↩︎