Symbol-crunching the Harborth graph

The Harborth graph is widely regarded as the smallest known example of a 4-regular planar unit-distance graph. In this paper we sketch an exact proof of this property, and present some of the minimal polynomials of the coordinates of the vertices of its most prominent embedding, the calculations of which give an example for the heavy use of computer algebra in the area of geometric graph theory. Finally we use the particular algebraic structure of these polynomials to deduce some geometric properties of the Harborth graph.