{"id":"palomar/PALOMAR-2026-10-01-000002","url":"https://github.com/akopjan/Palomar-Bang-Ball/tree/e57a2d8d0129b2d7ce3ee45c2064f5080c8c65eb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000002-v1.json","repo":"https://github.com/akopjan/Palomar-Bang-Ball","tags":["math.MG","msc:52A20","msc:52C17","msc:52A38","msc:52A40","convex-geometry","plank-theorem","lean","formalization"],"score":0,"title":"A Short Proof of Ball's Plank Theorem","trust":"high","domain":"math.MG","source":"palomar","authors":["Arseniy Akopyan"],"reviews":0,"subject":"math.MG","summary":"Formalization in Lean 4 of the paper 'A Short Proof of Ball's Plank Theorem' by Arseniy Akopyan and Alexander Polyanskii (arXiv:2609.36163). The paper gives a short proof of Keith Ball's 1991 theorem: if a centrally symmetric convex body in R^d is covered by finitely many planks, the sum of their relative widths with respect to the body is at least 1. The proof is based on a simple proof of a core theorem about linear functionals on R^n and an orthonormal basis. It also yields a short proof of Davenport's problem for centrally symmetric convex bodies (interior-disjointness of a homothet…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"A Short Proof of Ball's Plank Theorem","identifier":"https://arxiv.org/abs/2609.36163","relationship":"formalizes"}]}