Heilbronn's triangle problem
From OpenAI Aftermath
Heilbronn's triangle problem asks for Δ(n), the largest possible value of the smallest area of a triangle determined by n points in the unit square. Komlós, Pintz and Szemerédi disproved Heilbronn's original conjecture Δ(n) = O(n−2), and a weaker formulation asked whether Δ(n) ≤ Cεn−2+ε for every ε > 0. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a lower bound Δ(n) ≥ c1n−2+η with an absolute η > 0, which disproves that formulation. The collection includes a Lean formalization of a weaker form of this statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Erdős's finite-field parabola, recorded in Roth's 1951 paper, and random sampling with deletion both give Δ(n) ≫ n−2. Komlós, Pintz and Szemerédi improved this to Δ(n) ≫ (log n)/n2 through a hypergraph independence argument. The almost n−2 formulation is discussed in Zakharov's survey.
- On the upper-bound side, Roth proved the first o(n−1) estimate, with refinements by Schmidt and Roth; Komlós, Pintz and Szemerédi obtained n−8/7+ε, and Cohen, Pohoata and Zakharov obtained n−8/7−1/2000 and then n−7/6+ε.
- The manuscript states that earlier preprints by Ellmann and by Agama claiming stronger power lower bounds have unresolved issues in the versions it cites, and that its objections concern those arguments, not the impossibility of their bounds.
The original result
- Claim. Theorem 1.1 of A power improvement in the Heilbronn triangle lower bound states that there are absolute constants η, c1 > 0 and an integer n0 ≥ 3 such that Δ(n) ≥ c1n−2+η for every integer n ≥ n0, so the almost n−2 formulation fails at ε = η/2. Section 8 gives the explicit admissible exponent η = 2/(45435k + 16) for a fixed construction parameter k; the manuscript describes the exponent as extremely small and makes no attempt to optimize it.
- Method, as described: points are represented by integer columns in a box; each column receives a random label in a finite field, and the field norm of the finite-field parabola determinant is encoded in one designated coefficient of a determinant with base-B digit entries, so that distinct labels preclude a small determinant modulo a power of B. A random matrix of determinant one, lattice point counts for integral lifts, and a second congruence condition at an independent prime, using points of an affine quadratic surface with no three on a line, control the remaining cases including determinant zero; an elementary deletion argument completes the construction.
- Sources. The manuscript A power improvement in the Heilbronn triangle lower bound at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization constructs an unbounded sequence of sizes n and point sets for which every triangle has area at least n−2+η, for one fixed η > 0, and consequently refutes the proposed upper bound of order n−2+ε for every ε > 0. It adds that the linked construction is for an unbounded sequence of sizes and that the paper's statement for every sufficiently large n is broader. The Comparator statement is
HeilbronnTriangle.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "weaker-statement": the Lean theorem yields only an unbounded sequence of sizes, not every sufficiently large n, as the scope note states. The refutation of the almost n−2 bound is stated and follows from the subsequence, so only the uniformity in all large n is missing; the Lean exponent is an explicit, extremely small constant. It records a sandboxed Comparator pass. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | Ivan Blinov, littleBro/heilbronn-triangle-bounds (GitHub) | Extension (conditional) | A sequence of modifications of the construction, currently label tags in low digit positions, a fresh random digit when exactly two labels coincide, extension degree 5 and a shifted sphere packing, gives the conditional exponent η = 1/145,278,430 for every sufficiently large n. The README's table puts the manuscript's own exponent near 3.2·10−236; earlier versions of the repository stated smaller exponents such as 1/15,789,789,943. Lean proves the algebraic and finite parts, among them the degree-five norm decomposition, the packing, the scale inequalities and a finite digit probability theorem. | The README states that the full geometric theorem is conditional on the manuscript's estimates and the written transfer, that its Lean files prove neither those estimates nor the complete result, and that the draft, prepared with OpenAI Codex assistance, has no independent peer review. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the HeilbronnTriangle solution, in 701 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list HeilbronnTriangle, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor notes. The reviewer states that it read every section and checked each step by hand, including the lattice estimates, the norm polynomial and digit construction, the orbit counts, the auxiliary quadric, the zero-determinant cases, and the deletion and interpolation steps. | Part of an audit of the collection's manuscripts that the audit describes as complete. The review is published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
