HEXAGONbeta

A lower bound of 0.8366 for Lebesgue's universal covering problem

A mix of human-written and AI-generated textHuman understanding: all partsmath.MG — Metric Geometrycs.CG — Computational Geometrymath.NA — Numerical Analysis

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

A universal cover is a convex set in the plane that contains a congruent copy of every set of diameter at most 11. Lebesgue asked in 1914 for a universal cover of least area; before this work, the infimum Λ\Lambda of the areas of universal covers was known to satisfy 0.83474≤Λ≤0.84410.83474\le\Lambda\le0.8441. Lower bounds come from test sets: Λ\Lambda is bounded below by the least area of a convex hull of congruent copies of given sets of diameter at most 11. The best earlier lower bounds used the disk, the Reuleaux triangle and the Reuleaux pentagon, but these three bodies are known to admit a placement with hull area below 0.834790.83479, so they cannot give a much better bound. Adding the regular Reuleaux heptagon and nonagon of width 11, we improve the lower bound to Λ≥0.8366\Lambda\ge0.8366. Without the nonagon, the other four bodies already give Λ≥0.836\Lambda\ge0.836. The proof is a computer-assisted branch and bound over the relative placements of the bodies. Its certificates are checked in interval arithmetic, and separate proofs of both bounds in Lean 4, with their own certificates, are checked entirely by Lean's kernel.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.23717911

References

  1. J. C. Baez, K. Bagdasaryan and P. Gibbs, The Lebesgue universal covering problem , J. Comput. Geom. 6 (2015), 288--299.
  2. P. Brass, W. Moser and J. Pach, Research Problems in Discrete Geometry , Springer, New York, 2005.
  3. P. Brass and M. Sharifi, A lower bound for Lebesgue's universal cover problem , Internat. J. Comput. Geom. Appl. 15 (2005), 537--544.
  4. G. Elekes, Generalized breadths, circular Cantor sets, and the least area UCC , Discrete Comput. Geom. 12 (1994), 439--449.
  5. P. Gibbs, A new slant on Lebesgue's universal covering problem , arXiv:1401.8217, 2014.arXiv
  6. P. Gibbs, An upper bound for Lebesgue's covering problem , arXiv:1810.10089, 2018.arXiv
  7. H. C. Hansen, Small universal covers for sets of unit diameter , Geom. Dedicata 42 (1992), 205--213.
  8. J. Hatchett, Replay certificate for a 0.834740.83474 lower bound in Lebesgue's universal covering problem , software, Zenodo, 2026, doi:10.5281/zenodo.22135010 (https://doi.org/10.5281/zenodo.22135010), with a description in the repository https://github.com/newmattock/lebesgue-cover-0.83474-certificate.DOI
  9. F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic , IEEE Trans. Comput. 66 (2017), 1281--1292.
  10. H. Martini, L. Montejano and D. Oliveros, Bodies of Constant Width: An Introduction to Convex Geometry with Applications , Birkhäuser, Cham, 2019.
Show all 18 referencesShow fewer references
  1. The mathlib Community, The Lean mathematical library , in: Proc. 9th ACM SIGPLAN Int. Conf. Certified Programs and Proofs (CPP 2020), 2020, 367--381.
  2. U. Mishra, Curves of constant width and Lebesgue's covering problem , arXiv:2608.30538v2, 2026.arXiv
  3. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. 12699 , Springer, 2021, 625--635.
  4. J. Pál, Über ein elementares Variationsproblem , Danske Vid. Selsk. Mat.-Fys. Medd. 3 (1920), no. 2, 1--35.
  5. R. Sprague, Über ein elementares Variationsproblem , Mat. Tidsskr. B (1936), 96--99.
  6. T. Tao et al., Optimization constants in mathematics , https://teorth.github.io/optimizationproblems/, 2026.link
  7. N. Xie, A certified lower bound for Lebesgue's universal cover problem , arXiv:2606.04458, 2026.arXiv
  8. S. Zeng, An exact hierarchy for Lebesgue's universal covering constant and a certified 0.8340.834 lower bound , arXiv:2609.01284, 2026.arXiv

Version history

  1. v1 · 15 pagesSubmitted by Tejasvi Singh TomarPublished on Zenodo: https://doi.org/10.5281/zenodo.23717911CurrentNov 12, 2026