A power improvement in the Heilbronn triangle lower bound

1 paperLean

For every sufficiently large n, constructs n points in the unit square such that every triangle has area at least \(n^{-2+c}\) for one absolute c > 0. This disproves the conjectured almost-n⁻² upper bound in Heilbronn's triangle problem, which asks how large the smallest determined triangle can be.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A power improvement in the Heilbronn triangle lower bound

OpenAI · September 25, 2026

There are absolute constants \(\eta,c_1\gt 0\) such that, for every sufficiently large integer n, one can choose n points in the unit square so that every triangle they determine has area at least \(c_1n^{-2+\eta}\). Thus the almost n⁻² upper-bound formulation of Heilbronn's triangle problem is false. The exponent η is fixed but extremely small.

Read PDF Download Source

Cite

@misc{OAI:A-power-improvement-in-the-Heilbronn-triangle-lower-bound-September-25-2026,
  author = {{OpenAI}},
  title = {{A power improvement in the Heilbronn triangle lower bound}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-power-improvement-in-the-Heilbronn-triangle-lower-bound-September-25-2026/main.pdf}{OAI:A-power-improvement-in-the-Heilbronn-triangle-lower-bound-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A power improvement in the Heilbronn triangle lower bound

Scope

Heilbronn's triangle problem asks how large the smallest triangle determined by \(n\) points in the unit square can be. The formalization constructs an unbounded sequence of sizes \(n\) and point sets for which every triangle has area at least \(n^{-2+\eta}\), for one fixed \(\eta>0\). It consequently refutes the proposed upper bound of order \(n^{-2+\varepsilon}\) for every \(\varepsilon>0\). The linked construction is for an unbounded sequence of sizes; the paper's statement for every sufficiently large \(n\) is broader.

Comparator links

Result	Comparator statement
Power improvement for the smallest Heilbronn triangle	HeilbronnTriangle.lean

Scope note on GitHub →