tverberg_partition_conjecture
Provedcombinatoricsdiscretegeometrygeometrylogicnumber-theoryopenproblemprovedtopology
Tverberg's theorem: Any N=(r-1)(d+1)+1 points in ℝᵈ can be partitioned into r parts whose convex hulls intersect. The topological version (for continuous maps) is disproved for non-prime-power r; open for prime power r ≥ 4.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem tverberg_partition_conjecture (r d : ℕ) (hr : 2 ≤ r) (hd : 1 ≤ d) :
∀ (pts : Fin ((r - 1) * (d + 1) + 1) → EuclideanSpace ℝ (Fin d)),
∃ (partition : Fin r → Finset (Fin ((r-1)*(d+1)+1))),
(∀ i, (partition i).Nonempty) ∧
Finset.univ = Finset.biUnion Finset.univ partition ∧
(∀ i j, i ≠ j → Disjoint (partition i) (partition j)) ∧
(⋂ i : Fin r, convexHull ℝ
((partition i).image pts).toSet).Nonempty := by
sorrySource