Keller’s conjecture in $d$ dimensions states that there are no faceshare-free tilings of $d$-dimensional space by translates of a $d$-dimensional cube. In 2020, Brakensiek et al. resolved this 90-year-old conjecture by proving that the largest number of dimensions for which no faceshare-free tilings exist is 7. This result, as well as many others pertaining to Keller’s conjecture, critically relies on a reduction from Keller’s original conjecture to a statement about cliques in generalized Keller graphs. In this paper, we present a formalization of this reduction in the Lean 3 theorem prover. Additionally, we combine this formalized reduction with the verification of a large clique in the Keller graph $G_8$ to obtain the first verified end-to-end proof that Keller’s conjecture is false in 8 dimensions.
Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 18:00 | Formalized Mathematics ICPP at Studio 1 Chair(s): Adam Chlipala Massachusetts Institute of Technology | ||
16:00 22mTalk | Formalising the h-principle and sphere eversionremote presentation CPP | ||
16:22 22mTalk | A Formalized Reduction of Keller's Conjecture CPP Joshua Clune Carnegie Mellon University | ||
16:45 22mTalk | Computing Cohomology Rings in Cubical Agdadistinguished paper CPP Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay, Axel Ljungström Stockholm University, Anders Mörtberg Department of Mathematics, Stockholm University | ||
17:07 8mBreak | short break CPP | ||
17:15 45mMeeting | CPP Business Meeting CPP Pre-print | ||