HEXAGONbeta

Lower bounds for the Beardwood–Halton–Hammersley constant

A mix of human-written and AI-generated textHuman understanding: all partsmath.PR — Probabilitymath.OC — Optimization and Controlmath.MG — Metric Geometrymath.NA — Numerical Analysis

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

Let β\beta be the Beardwood–Halton–Hammersley constant: the shortest tour through nn independent uniform random points in the unit square has length asymptotic to βn\beta\sqrt n almost surely. Dong and Cao proved β≥0.6421\beta\ge0.6421 from an inequality β≥5/8+∑k=3KCk\beta\ge5/8+\sum_{k=3}^{K}C_k, where CkC_k is an integral over configurations of kk points in the plane that form a connected graph when points at distance at most 11 are joined. For C3C_3, C4C_4 and C5C_5, sharper bounds come from a first-order expansion of the area of the union of the unit disks on boxes of configurations. For C6+⋯+C22C_6+\dots+C_{22}, which Dong and Cao did not use, a lower bound comes from comparing each point only with the three points before it in the order of their first coordinates. We obtain β≥0.6496\beta\ge0.6496, and β≥0.6508\beta\ge0.6508 if the exponential function of the C library used to evaluate the bound for C6+⋯+C22C_6+\dots+C_{22} has a relative error below 10−910^{-9}. The proofs are computer-assisted; the bound 0.64960.6496 is proved in Lean 4, with finite checks evaluated by compiled code, from the inequality of Dong and Cao and two statements about unions of disks that we prove but do not formalize.

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

References

  1. J. Beardwood, J. H. Halton and J. M. Hammersley, The shortest path through many points , Proc. Cambridge Philos. Soc. 55 (1959), 299--327.
  2. M. Carneiro, Lean4Lean: verifying a typechecker for Lean, in Lean , arXiv:2403.14064, 2024.arXiv
  3. W. Cook, In Pursuit of the Traveling Salesman: Mathematics at the Limits of Computation , Princeton University Press, Princeton, 2012.
  4. Z. Dong and J. Cao, New bounds for the Euclidean TSP constant , arXiv:2610.02809v1, 2026.arXiv
  5. The FLINT team, FLINT: Fast Library for Number Theory , version 3, https://flintlib.org.link
  6. The GNU C Library Reference Manual, Section 19.7, Errors in Math Functions , https://sourceware.org/glibc/manual/.link
  7. J. Gaudio and P. Jaillet, An improved lower bound for the traveling salesman constant , Oper. Res. Lett. 48 (2020), 67--70.
  8. F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic , IEEE Trans. Comput. 66 (2017), 1281--1292.
  9. D. S. Johnson, L. A. McGeoch and E. E. Rothberg, Asymptotic experimental analysis for the Held--Karp traveling salesman bound , in: Proc. 7th ACM-SIAM Symposium on Discrete Algorithms, 1996, 341--350.
  10. The mathlib Community, The Lean mathematical library , in: Proc. 9th ACM SIGPLAN Int. Conf. Certified Programs and Proofs (CPP 2020), 2020, 367--381.
Show all 14 referencesShow fewer references
  1. 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.
  2. nanoda_lib , a type checker for Lean 4, https://github.com/ammkrn/nanoda_lib.link
  3. S. Steinerberger, New bounds for the traveling salesman constant , Adv. in Appl. Probab. 47 (2015), 27--36.
  4. T. Tao et al., Optimization constants in mathematics , https://teorth.github.io/optimizationproblems/, 2026.link

Version history

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