Papers With

← All papers
First page of The affine Tverberg theorem revisited

The affine Tverberg theorem revisited

Sergey Avvakumov, Roman Karasev

math.CO Sep 11, 2026 · v1 math.MG
formalization combinatorics geometry
Read PDF arXiv abstract Code
TL;DR
The proof of the main theorem (Tverberg's theorem for polytopes and simplicial balls) was formalized and checked in Lean 4, with a public repository.
Abstract
We prove the Bárány–Kalai–Tverberg conjecture extending the affine version of Tverberg's theorem to simplicial balls and polytopes other than the simplex: For any affine map $φ: P\to \mathbb R^d$ from a convex polytope $P$ of dimension $N=(d+1)(r-1)$ with $r\geq 2$, there exist $r$ pairwise disjoint faces $F_1,\ldots,F_r\subset\partial P$ such that $φ(F_1)\cap\dots\capφ(F_r)\neq\varnothing$. A similar statement holds for a simplicial ball $P$ with $φ$ assumed affine on all of its faces.
Problem

The Bárány–Kalai–Tverberg conjecture asks whether the affine Tverberg theorem extends from the simplex to arbitrary convex polytopes and simplicial balls of dimension N=(d+1)(r-1). Standard equivariant methods fail when r is not a prime power.

Approach

The affine map is lifted to a map from the r-fold join to R^N, and the problem is reduced to showing that 0 lies in the image of the deleted join. The proof combines a Leray–Vietoris–Begle type lemma, a bad-vertex triangulation, and acyclicity arguments over shellable polytopal subdivisions arising from the upper hull of an auxiliary polytope. The proof was formalized in Lean 4.

Results

The conjecture is proved for all r ≥ 2. For any affine map from an N-dimensional polytope, or a face-wise affine map from a simplicial ball, there are r pairwise disjoint boundary faces whose images intersect. The formalization is available at github.com/savvakumov/AffineTverberg.