Tverberg's theorem

tverberg_theorem

Submitter: Kim Morrison.

Notes: Any (r-1)(d+1)+1 points in ℝ^d can be partitioned into r parts whose convex hulls share a common point. Trusted helper HasTverbergPartition (non-hole). Mathlib has Radon's theorem (the r=2 case) but not Tverberg. Candidate from §169 of the Knill survey.

Source: H. Tverberg, *A generalization of Radon's theorem*, J. London Math. Soc. 41 (1966). Knill, §169.

Informal solution: Unavailable.

theorem declaration uses `sorry`tverberg_theorem (d r : ℕ) (hr : 1 ≤ r)
    (f : Fin ((r - 1) * (d + 1) + 1) → LeanEval.Combinatorics.Tverberg.Space d) :
    LeanEval.Combinatorics.Tverberg.HasTverbergPartition (r := r) f := byd:ℕr:ℕhr:1 ≤ rf:Fin ((r - 1) * (d + 1) + 1) → Space d⊢ HasTverbergPartition f
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026