A Formalized Reduction of Keller's Conjecture

on YouTube ↗22m

" summary

Formalization produces a machine-checked reduction from the infinite geometric statement of Keller’s conjecture to a finite graph problem, encodes d-dimensional unit cubes and periodic tilings, and proves equivalence to cliques in generalized Keller graphs; combining a verified brute-force check of a clique of size 2^8 in G_8 (checked via generated Lean 3 code) yields the first end-to-end formal proof that Keller’s conjecture is false in 8 dimensions.

AI-written summary · about

" chapters (10)

1. 0:00Keller's Conjecture intro
2. 0:23What is Keller's Conjecture
3. 2:48Keller's Conjecture higher dims
4. 3:50Geometric reduction formalized
5. 7:02Reducing to periodic tilings
6. 11:17Color graphs introduction
7. 13:22Tilings to graph cliques
8. 16:338D verification results
9. 17:597D verification future
10. 18:46Q&A