山本 光晴

Among many fields of mathematics and computer science, discrete mathematics is one of the most difficult fields to formalize because we prove theorems using intuitive inferences that have not been rigorously formalized yet. This paper focuses on graph theory from discrete mathematics and formalizes planar graphs. Although planar graphs are usually defined by embeddings into the two-dimensional real space, this definition can hardly be used for actually developing a formal theory of planar graphs. In this paper, we take another approach we inductively define planar graphs and prove their properties based on the inductive definition. Before the definition of planar graphs, the theory of cycles is also introduced and used as a foundation of planar graphs. As an application of the theory of planar graphs, Euler's formula is proved.