Tverberg's theorem

tverberg_theorem — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Tverberg's theorem.** Any `(r-1)(d+1)+1` points in `ℝ^d` admit an
`r`-part Tverberg partition. -/
theorem tverberg_theorem (d r : ℕ) (hr : 1 ≤ r)
    (f : Fin ((r - 1) * (d + 1) + 1) → Space d) :
    HasTverbergPartition (r := r) f := by
  sorry

Source

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

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: tverberg_theorem
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.