{"id":"palomar/PALOMAR-2026-09-03-000003","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/d932843c58b449bfc1172686ddeef94945eb3c57","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-03-000003-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.MG","math.CO","msc:52A35","msc:52C10","msc:52A20","convex-geometry","tverberg-theorem","lean-formalization"],"score":0,"title":"Tverberg's Partition Theorem, 1D Theorem, and Colorful 1D Theorem","trust":"high","domain":"math.MG","source":"palomar","authors":["Noah Cohen"],"reviews":0,"subject":"math.MG","summary":"A complete, machine-checked Lean 4 formalization of Tverberg's Theorem (Helge Tverberg, 1966) in the distinct-point set formulation across dimensions d >= 1 (with d = 0, r > 1 cases vacuously satisfied due to Finset carrier capacity limits on Fin 0 -> ℝ) via the Sarkaria–Bárány Colorful Carathéodory reduction, the full 1D Tverberg theorem for arbitrary r via symmetric-rank pairing following Mulzer–Werner, and the 1-dimensional Colorful Tverberg Theorem for arbitrary r (Bárány–Larman–Pach 1992). Proves that any (r - 1)(d + 1) + 1 points in ℝ^d can be partitioned into r parts whose convex…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"A generalization of Radon's theorem","identifier":"","relationship":"formalizes"},{"title":"Tverberg's theorem via number fields","identifier":"","relationship":"formalizes"},{"title":"A generalization of Carathéodory's theorem","identifier":"","relationship":"formalizes"},{"title":"Approximating Tverberg points in linear time for any fixed dimension","identifier":"","relationship":"adapts"},{"title":"Radon-partition property in topological affine spaces","identifier":"","relationship":"formalizes"}]}