AI Proof WatchKeep up with AI contributions

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.

Sources for this record

What was already known

Chazelle proved linear-time triangulation in 1991, with a general-position assumption handled by perturbation. This project supplies a formally checked program with explicit degeneracy and word specifications.

AI involvement AI-led

Robert D. Barish set the task and direction. Claude agents designed the variant RAM program and specification and developed its Lean proof; an unidentified OpenAI model may have helped early on. Barish audited attribution, while no line-by-line human proof review is documented.

AI agents designed the exact RAM implementation and proved its bounds under human task direction; the exact model mix in the earliest stage is unresolved.

Importance Notable

Formally verifies an explicit linear-time triangulation program for a difficult established result.

Limitations

The constants are extremely large. The theorem does not give a cost bound for Chazelle’s paper algorithm verbatim or prove its visibility-map conclusion.

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

The repository reports Lean kernel checking, permitted-axiom audits, Comparator statement agreement and independent kernel replays for the cited program theorem. This review did not rerun the large development; paper-to-algorithm fidelity remains a human interpretation.

Formal checking

compiled proof terms, axiom and statement audits, independent kernel replay

Checker
Lean kernel; NanoDa, con-ron, leanchecker, lean4lean and con-leche replay tools
Scope
The linear-time triangulation statement and named-program correctness and refinement theorems for the stated version.
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

No named human explanation or line-by-line human review of this very large proof is documented. Few is the evidence-gap default, not a claim that Barish lacks understanding.

Correction and publication history

2026-10-18 · publication

Formally verifies an explicit linear-time triangulation program for a difficult established result.

Read this published revision