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.
|Title of host publication||Lecture Notes in Computer Science|
|Publication status||Published - 1 Jan 2010|
|Event||International Congress on Mathematical Software (ICMS) - |
Duration: 1 Jan 2010 → …
|Conference||International Congress on Mathematical Software (ICMS)|
|Period||1/01/10 → …|