To­wards a proof of Euler's poly­he­dron for­mu­la for Math­lib

As part of my doc­tor­al dis­ser­ta­tion, I de­vel­oped a for­mal proof, in the Mizar sys­tem, of Euler's poly­he­dron for­mu­la. That's the re­sult in math­e­mat­ics (com­bi­na­to­r­i­al topol­o­gy) which says that, for a poly­he­dron $p$, we have

where $V$, $E$, and $F$ are, re­spec­tive­ly, the num­bers of ver­tices, edges, and faces of $p$.

To get a feel for that fact, take a look at the pla­ton­ic solids (tetra­he­dron, cube, oc­ta­he­dron, do­dec­a­he­dron, and icosa­he­dron). But that's just the be­gin­ning; the for­mu­la is true of all con­vex poly­he­dra, and some more too. There are some ex­ten­sions of the the­o­rem for non-con­vex poly­he­dra, and it can be gen­er­al­ized to ar­bi­trary fi­nite di­men­sions. (The 2-di­men­sion­al ver­sion of the the­o­rem says that $V=E$ for a poly­gon. Neat!)

Lean cur­rent­ly doesn't have a proof of Euler's poly­he­dron for­mu­la. It's one of the few the­o­rems in Freek Wiedijk's 100 The­o­rems that's still out­stand­ing in Lean.

So I de­cid­ed to give it a go.

With some as­sis­tance from Claude Code, Loogle, Leansearch, and just bread-and-but­ter dig­ging around in Math­lib, I was able to whip to­geth­er a proof of Euler's poly­he­dron for­mu­la for com­bi­na­to­r­i­al poly­he­dra, which are just a fi­nite se­quence of in­ci­dence re­la­tions: we pos­tu­late fi­nite sets of ver­tices, edges, etc. and say which ver­tices are in­ci­dent with which edges, which edges with which faces, etc. Fol­low­ing the stan­dard ap­proach in al­ge­bra­ic topol­o­gy, we de­fine a bound­ary op­er­a­tor (es­sen­tial­ly, which are the edges that go around a sin­gle face, which are the two ver­tices of a sin­gle edge). The no­tion of bound­ary gets gen­er­al­ized a bit to map sets of faces (or edges) to a set of edges (or ver­tices). Math­e­mat­i­cal­ly, what's go­ing s that we're work­ing over fi­nite-di­men­sion­al vec­tor spaces over $Z_2$ gen­er­at­ed by the faces, edges, and ver­tices; the bound­ary op­er­a­tors are lin­ear trans­for­ma­tions from these spaces. The con­nec­tion from the (ab­stract, com­bi­na­to­r­i­al) geom­e­try to the al­ter­nat­ing sum $V$$-$$E$$+$$F$ comes from us­ing the rank-nul­li­ty the­o­rem. in lin­ear al­ge­bra.

Al­though I've been fol­low­ing Lean for a cou­ple years now, I've gen­er­al­ly been noth­ing more than a tourist vis­it­ing a friend­ly place I want to learn more about. I'm a big fan; I even or­ga­nize a con­fer­ence ded­i­cat­ed to it! I've been want­i­ng to dip my toes in—or, rather, jump in—for a while, and a nat­ur­al start­ing point, for me, is to re­vis­it a math­e­mat­i­cal re­sult I had al­ready for­mal­ized (check­ing, of course, that it doesn't al­ready ex­ist in Math­lib). In fact, my real aim isn't nec­es­sar­i­ly con­tribut­ing to Math­lib, but work­ing on soft­ware ver­i­fi­ca­tion with Lean. But con­tribut­ing to Math­lib is prob­a­bly a good first step.

Af­ter get­ting some­thing that worked, I opened a PR against Math­lib and post­ed a re­quest for re­view on the Lean Zulip.

I quick­ly found out that my new­bie PR need­ed work. I end­ed up fac­tor­ing out one of the core al­ge­bra­ic topo­log­i­cal re­sults, the Euler-Poin­caré for­mu­la, into its own PR. Also, re­flect­ing on the feed­back that my pure­ly com­bi­na­to­r­i­al for­mal­iza­tion of poly­he­dra doesn't re­late to Eu­clid­ean space or real num­bers at all, I de­cid­ed to close my PR and go back to the draw­ing board. I'm cur­rent­ly work­ing on a va­ri­ety of top­ics cen­tered around Euler's poly­he­dron for­mu­la. I'm ul­ti­mate­ly work­ing on a ver­sion of Euler's poly­he­dron for­mu­la for con­vex poly­he­dra (which con­nect­ed with real num­bers). The plan there is to de­vel­op a the­o­ry of con­vex poly­topes to the point where we can as­so­ciate a chain com­plex with one, show that they're ho­mol­o­gy spheres, and then ap­ply the Euler-Poin­caré for­mu­la.

I'll also keep push­ing in this area. It's a de­light to use Claude Code and al­lied tools to help do these for­mal­iza­tions. The won­der­ful Lean LSP MCP col­lec­tion (dare I call it a the­o­rem prover?) is a real pow­er tool. I'd like to have a ver­sion of Euler's poly­he­dron for­mu­la based on com­bi­na­to­r­i­al maps and per­haps CW com­plex­es.