Email Gateway (Sep 11 2026 at 19:46): Email Gateway (Sep 11 2026 at 19:46):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce yet another of the 100 theorems: The Five Platonic Solids
by Evan Finken
This entry formalizes that there are exactly five Platonic solids: the tetrahedron, cube, octahedron, dodecahedron, and icosahedron. A Platonic solid is a convex polyhedron whose faces are congruent regular polygons, with the same number of edges meeting at each vertex. Euler's polyhedron formula is used to show that there are at most five Platonic solids, and each of the five, defined as the convex hull of its vertices, is then shown to satisfy the required properties. The formal proof is computational (slow!) and is ported from John Harrison's formalization in HOL Light.
https://isa-afp.org/entries/Platonic_Solids.html
Larry
Last updated: Sep 17 2026 at 22:43 UTC