Papers With

← All papers
cs.LO

A Formalized Reduction of Keller's Conjecture

Joshua Clune

cs.LO Jan 16, 2023 · v1
formalization combinatorics geometry
Read PDF arXiv abstract
TL;DR
Formalizes in Lean the reduction of Keller's conjecture to a finite clique-finding problem.
Abstract
This paper presents a formalized proof in Lean that reduces Keller's conjecture to a finite combinatorial problem. Keller's conjecture states that in any tiling of n-dimensional space by unit cubes, some pair must share an entire (n-1)-dimensional face. The author formalizes the reduction showing that the conjecture for dimension n is equivalent to the nonexistence of certain cliques in the Keller graph, enabling the use of computational verification to settle the conjecture.
Problem

Keller's conjecture (that in any tiling of n-dimensional space by unit cubes, some pair must share an entire face) had a known reduction to a combinatorial clique problem, but no formalized proof of this reduction existed.

Approach

The author formalizes in Lean the reduction showing that Keller's conjecture for dimension n is equivalent to the nonexistence of certain cliques in the Keller graph. This enables computational verification (SAT solvers) to settle the conjecture for specific dimensions once the reduction is trusted at the formal level.

Results

A complete formalized Lean proof of the reduction from Keller's conjecture to the finite combinatorial clique problem is produced, removing any trust gap between the mathematical reduction and the computational verification that settles the conjecture.