REU Project

There is a growing effort to formalise mathematical knowledge in modern proof assistants, with Lean and the mathlib library playing a central role. Most areas of undergraduate mathematics are already covered well. However, graph theory is a subject which is still relatively underdeveloped in mathlib. We survey what in the field has been done and how and give examples of the various difficulties the formalisation of graphs poses in an attempt to understand this disparity. Then we present our own contribution, developing a formal environment for planar simple graphs in Lean with the aim of keeping its use intuitive and minimising the artifacts caused by the strict type-checking nature of this language. The description of planarity we use is combinatorial, via rotation systems. We demonstrate the practicality of our work by proving that the disjoint union of planar graphs is planar with the tools we develop. The proof includes a description of the connected components of a disjoint union, which is also a previously unformalised result.