A Discrete Aspect of the Kervaire-Laudenbach Conjecture

Potential supervisors: 


This proposal concerns aspects of the Kervaire-Laudenbach conjecture. Even though this conjecture is phrased in the language of group theory, we will be interested in a special case that can be expressed without referring to groups at all. Thus, no knowledge of group theory is needed for this master thesis. Instead, you will be working with planar graphs, a basic discrete object important in many areas of computer science.

Kervaire-Laudenbach Conjecture. Let G be a group. Any equation a₁ x^{e₁} ... aₙ x^{eₙ} = 1 with coefficients aᵢ ∈ G and non-zero sum of exponents eᵢ ∈ {-1, 1} has a solution x in some group which contains G.

While this conjecture remains unsolved, special cases have been known for some time.

This proposal concerns the case of a torsion-free group G proven in [1]. In that case, the problem follows from the following combinatorial property of planar graphs.

Theorem A. Consider an n-gon P with corners labelled in clockwise order by formal symbols a₁, …, aₙ and edges oriented according to the values of e₁, …, eₙ. Consider also the “mirror image” P' of P, with corner label aᵢ replaced by aᵢ'. Let K be an arbitrary directed connected planar graph whose faces are built out of topological copies of P and P'. Then there are two vertices x for which there is an i such that the corners of x are labelled using only aᵢ or aᵢ'.

Klyachko [1] observed that this theorem follows from a beautiful topological property of connected planar graphs, which has been called the “car crash theorem” (see [2] for a good exposition). He writes:

This fact is so simple and funny that [it] can be included in a collection of puzzles or suggested as a problem for a school mathematical tournament.

Car crash theorem (informal). For each face of a connected planar graph, let a car be travelling along its boundary in clockwise order, continuously, without stops, and visiting every point of the boundary infinitely often. Then there are two different points P at which a /complete crash/ will happen, meaning that all cars of the faces whose boundaries contain P are at that point at the same time.

Note that P can be an interior point of an edge, meaning the crash involves two cars, or a vertex, meaning the number of cars crashing is the degree of the vertex.

The crash theorem is phrased in the language of analysis, referring to continuous motions of cars indexed by real numbers, and its proof uses the axiom of exluded middle. This makes it unsuitable for formalization in the constructive setting of proof assistants such as Agda. However, the crash theorem is applied in a completely discrete situation. This is evidence that the use of analytic objects is redundant. Hence, there should be a constructive, discrete analogue of the crash theorem, like Sperner's lemma [3] is the discrete analogue of Brouwer's fixed-point theorem [4]. Such a discrete version would be suitable for formalization in Agda.

The Project

The task is to find, prove, and formalize in Agda the discrete crash theorem. This can be broken down as below.

  1. Find and state the “discrete crash theorem”, the discrete analogue of the crash theorem. The theorem should be strong enough that Theorem A can be deduced from it just like from the continuous crash theorem.
  2. Prove the discrete crash theorem in an entirely discrete combinatorial manner. This means you should avoid analytic objects such as real numbers. The proof will be constructive and involve inductive arguments on connected planar graphs.
  3. Formalize the notion of connected planar graph in Agda. You will have to come up with a suitable representation as a data type that includes the topological aspect. For an example of such a representation in Haskell, see [5]. Formalize various basic properties of connected planar graphs needed in the next step.
  4. Formalize the discrete crash theorem and its proof in Agda.

Since (1.) involves original research, it is open how much time will be needed there. It will be possible to adjust goals according to the complexity of the problem.

Note that (3.) can be completed independently of (1.) and (2.). The type-based feedback you get in (3.) and (4.) may help you in completing (1.) and (2.) as elegantly as possible.


  • You should have attended the course "Types for Programs and Proofs", or otherwise be familiar with Agda.
  • You should know basic graph theory, in particular be familiar with planar graphs.
  • Knowledge of group theory is not required.
  • A basic mathematical background, for example familiarity with proofs by induction, is expected.


[1] A funny property of sphere and equations over groups
[2] Klyachko's methods and the solution of equations over torsion-free groups
[3] Sperner's lemma
[4] Brouwer fixed-point theorem
[5] The planar-graph package

Date range: 
January, 2018 to January, 2023