HEXAGONbeta

A converse to the discrete four-vertex theorem

A mix of human-written and AI-generated textHuman understanding: all partsmath.MG — Metric Geometrymath.DG — Differential Geometry

Contributed by Kristoffer Josefsson ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

Tabachnikov asked whether every cyclic sequence of positive numbers with at least two local maxima and two local minima is the sequence of radii of the circles through consecutive vertex triples of a convex polygon whose circumcenters lie inside the corresponding vertex angles. We prove this for every n ≥ 4, with extrema counted as plateaus. This is the sharp form: by Dahlberg’s discrete four-vertex theorem the condition is also necessary for nonconstant sequences. Locally near every nonconstant admissible sequence the polygon can be chosen to depend continuously (indeed C1) on the sequence, but in general not globally: we give an explicit path of admissible hexagon data along which no continuous choice of realizing polygons exists. The existence and continuity results are formalized in Lean 4 with Mathlib. We also prove the corresponding characterization for circles tangent to three consecutive supporting lines, using a separate tangential-polygon construction and Wegner’s forward theorem.

Provenance statement

A full Lean formalization of the work as well as all of it's assumptions are provided

Formalizations

Tools used

Lean
Lean
Anthropic
Claude Fable
OpenAI
Codex

References

  1. Bilinski, Stanko. Die primitivste Form des Vierscheitelsatzes. Glasnik Mat.-Fiz. Astronom. Društvo Mat. Fiz. Hrvatske Ser. II, vol. 18, pp. 85–93. 1963
  2. Dahlberg, Björn E. J. The converse of the four vertex theorem. Proc. Amer. Math. Soc., vol. 133, no. 7, pp. 2131–2135. 2005. https://doi.org/10.1090/S0002-9939-05-07788-9DOI
  3. Dahlberg, Björn E. J. A discrete four vertex theorem. Geom. Dedicata, vol. 133, pp. 111–128. 2008. https://doi.org/10.1007/s10711-008-9238-0DOI
  4. DeTurck, Dennis; Gluck, Herman; Pomerleano, Daniel; Vick, David Shea. The four vertex theorem and its converse. Notices Amer. Math. Soc., vol. 54, no. 2, pp. 192–207. 2007. https://arxiv.org/abs/math/0609268link
  5. Gluck, Herman. The converse to the four vertex theorem. Enseign. Math. (2), vol. 17, pp. 295–309. 1971. https://doi.org/10.5169/seals-44584DOI
  6. Josefsson, Kristoffer. Lean formalization of converse four-vertex theorems. 2026. https://github.com/kejace/cd4vtlink
  7. Musin, Oleg R. Curvature extrema and four-vertex theorems for polygons and polyhedra. J. Math. Sci. (N.Y.), vol. 119, no. 2, pp. 268–277. 2004. https://doi.org/10.1023/B:JOTH.0000008769.58818.6d; Revised version: arXiv:0805.0629v3 (https://arxiv.org/abs/0805.0629v3)arXivDOI
  8. Ovsienko, Valentin; Tabachnikov, Serge. Projective geometry of polygons and discrete 4-vertex and 6-vertex theorems. Enseign. Math. (2), vol. 47, no. 1–2, pp. 3–19. 2001. https://doi.org/10.5169/seals-65426; arXiv:math/9909150 (https://arxiv.org/abs/math/9909150)arXivDOI
  9. Pak, Igor. Lectures on Discrete and Polyhedral Geometry. 2010. Draft, April 20, 2010; https://www.math.ucla.edu/~pak/geompol8.pdflink
  10. Sedykh, Vyacheslav D. Discrete versions of the four-vertex theorem. Topics in Singularity Theory, vol. 180, pp. 197–207. 1997. https://doi.org/10.1090/trans2/180/17DOI
Show all 13 referencesShow fewer references
  1. Tabachnikov, Serge. A four vertex theorem for polygons. Amer. Math. Monthly, vol. 107, no. 9, pp. 830–833. 2000. https://doi.org/10.1080/00029890.2000.12005277DOI
  2. Tabachnikov, Serge. Converse Sturm–Hurwitz–Kellogg theorem and related results. J. Fixed Point Theory Appl., vol. 3, no. 1, pp. 121–130. 2008. https://doi.org/10.1007/s11784-007-0049-y; arXiv:0710.5902 (https://arxiv.org/abs/0710.5902)arXivDOI
  3. Wegner, Bernd. On the evolutes of piecewise linear curves in the plane. Rad Hrvatske Akad. Znan. Umjet. Mat. Znan., vol. 11 (467), pp. 1–16. 1994. https://dizbi.hazu.hr/?pr=i&id=172424link

Version history

  1. v1Submitted by Kristoffer JosefssonInitial depositCurrentOct 17, 2026