Prove2Me

tetrahedron_packing_density

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

geometryoptimization

Optimal tetrahedron packing: What is the densest packing of regular tetrahedra in ℝ³? Best known: density 100/117 ≈ 0.8547 by Kallus et al. (2010), improved to ≈ 0.856347 by Chen (2008). Optimal density unknown.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem tetrahedron_packing_density :
    ∃ (density : ℝ), density > 0.856347 ∧ density ≤ 1 ∧
    ∃ (centers : ℕ → EuclideanSpace ℝ (Fin 3))
      (orientations : ℕ → Matrix (Fin 3) (Fin 3) ℝ),
      ∀ i j : ℕ, i ≠ j → True := by
  sorry
Source
https://en.wikipedia.org/wiki/Tetrahedron_packing

View graph