Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Euler's Polyhedron Formula by ...

Email Gateway (Sep 22 2023 at 11:21):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’d like to announce a new AFP entry.

Euler's Polyhedron Formula
by Lawrence C. Paulson

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.

https://www.isa-afp.org/entries/Euler_Polyhedron_Formula.html

Enjoy,
René

Last updated: Jan 04 2025 at 20:18 UTC