Euler's polyhedron formula in Mizar

DI Group Author

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)


Euler’s polyhedron formula asserts for a polyhedronpthatV − E + F = 2, whereV,E, andFare, respectively, the numbers of vertices, edges, and faces ofp. Motivated by I.Lakatos’s philosophy of mathematics as presented in hisProofs and Refutations, in which the history of Euler’s formula is used as a case study to illustrate Lakatos’s views, we formalized a proof of Euler’s formula formula in themizarsystem. We describe some of the notable features of the proof and sketch an improved formalization in progress that takes a deeper mathematical perspective, using the basic results of algebraic topology, than the initial formalization did.
Original languageUnknown
Title of host publicationLecture Notes in Computer Science
EditorsK Fukada
ISBN (Print)978-3-642-15581-9
Publication statusPublished - 1 Jan 2010
EventInternational Congress on Mathematical Software (ICMS) -
Duration: 1 Jan 2010 → …


ConferenceInternational Congress on Mathematical Software (ICMS)
Period1/01/10 → …

Cite this