The Affine Plank Conjecture concerns planks covering convex bodies.
A convex body is any shape that has no inward curves. Here's an example of a body that's not convex:
A plank is a region between two parallel planes (or two parallel lines in the plane). The relative width of a plank is the plank's width divided by the width of the convex body perpendicular to the plank:
In 1951 Thøger Bang conjectured that if planks cover a convex body, their relative widths must sum to at least 100%:
You can play around with this in the interactive visualization.
This became known as the Affine Plank Conjecture. The papers below address the case of three planks in the plane, which had remained open for 75 years. The general conjecture remains open.
Three planks
These papers give proofs for triangles and for general convex bodies in the plane. Each has an accompanying Lean formalization.
- An elementary proof
of the affine plank conjecture for three planks on a triangle
A short proof for triangles using elementary geometry. - The affine plank
theorem for three planks in the plane
A proof for any convex body in the plane.
Acknowledgements
I'd like to thank Fedor Nazarov for introducing me to the problem, Kevin Barreto for inspiring me to tackle ambitious mathematical problems with LLMs and proof assistants, and the ARIA Safeguarded AI programme for providing funding for LLM usage.