Euler's Polyhedron Formula

Lawrence C. Paulson 📧

September 16, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Euler stated in 1752 that every convex polyhedron satisfied the formula $V - E + F = 2$ where $V$, $E$ and $F$ are the numbers of its vertices, edges, and faces. For three dimensions, the well-known proof involves removing one face and then flattening the remainder to form a planar graph, which then is iteratively transformed to leave a single triangle. The history of that proof is extensively discussed and elaborated by Imre Lakatos, leaving one finally wondering whether the theorem even holds. The formal proof provided here has been ported from HOL Light, where it is credited to Lawrence. The proof generalises Euler's observation from solid polyhedra to convex polytopes of arbitrary dimension.


BSD License


Related publications

  • Lawrence, J. (1997). A Short Proof of Euler’s Relation for Convex Polytopes. Canadian Mathematical Bulletin, 40(4), 471–474.
  • Wikipedia

Session Euler_Polyhedron_Formula