Exact linear-time triangulation of simple polygons

Can an explicit exact-real-RAM program triangulate every closed simple n-vertex polygon, including collinear vertices and equal heights, with n−2 conforming triangles in at most C(n+1) steps and natural-word storage bounded by K(n+1)? The scoped verification target is the specified variant of Chazelle’s linear-time construction.

Why it matters and what counts as progress

Why it matters: It asks for a completely explicit, verified linear-time realization of polygon triangulation, including geometric degeneracies and storage bounds.

What counts as progress: An explicit triangulation algorithm with proved linear running time, storage and geometric correctness, including degenerate vertex configurations.

How the problem developed

1991 · Algorithm [1]
Bernard Chazelle Published a linear-time algorithm for triangulating simple polygons.
5 Oct 2026 · Formal proof [2][3][4]
Robert D. Barish, with AI coding agents mainly from Claude under his direction Registered a Lean-verified exact real-RAM program with linear time and space-word bounds for triangulating every simple polygon. The implementation is a variant of Chazelle’s algorithm, not the paper’s program verbatim; the author says some earliest work may have used an OpenAI model.

AI contribution

AI-built Lean program triangulates simple polygons in linear time

For every closed simple polygon with n vertices, including collinear vertices and equal heights, an explicit exact-real-RAM program returns a conforming triangulation with n−2 triangles in at most C(n+1) steps and natural words bounded by K(n+1). It is a variant of Chazelle’s algorithm that completes the visibility map directly below n=2³⁰+2.

AI involvementAI-led

ImportanceNotable

Technical verificationFormal (Lean 4/Mathlib kernel, Comparator, and independent kernel replays)

Human understandingFew