---

Claim. OpenAI, A power improvement in the Heilbronn triangle lower bound, OpenAI Math Release preprint, 25 September 2026, linked above at the pinned revision and carded in the library (card). For a finite set $P$ of at least three points in the unit square let $\Delta(P)$ be the least area of a triangle with vertices in $P$, collinear triples counting as area zero, and let $\Delta(n)$ be the largest $\Delta(P)$ over sets of $n$ points. The paper's Theorem 1.1 states that there are absolute constants $\eta,c_1>0$ and an integer $n_0\ge3$ with

$$\Delta(n)\ge c_1\,n^{-2+\eta}\qquad\text{for every integer }n\ge n_0 .$$

This improves the lower bound $\Delta(n)\gg(\log n)/n^2$ of Komlós, Pintz and Szemerédi [KPS82] by a power of $n$, and it refutes the almost-$n^{-2}$ formulation of Heilbronn's problem discussed in Zakharov's survey, which asks whether $\Delta(n)\le C_\varepsilon n^{-2+\varepsilon}$ holds for every $\varepsilon>0$ and all large $n$: the theorem contradicts it at $\varepsilon=\eta/2$. The exponent is explicit (the paper's formula (8.7)) but extremely small, and the paper makes no attempt to optimize it. The construction labels integer columns in a box by elements of a finite field of odd degree over $\mathbb F_r$, uses the norm polynomial of the finite-field parabola behind Erdős's $n^{-2}$ construction, encoded in one coefficient of a base-$B$ expansion in the manner of the Salem–Spencer and Behrend constructions, so that distinct labels force a large determinant modulo a power of $B$; a random unimodular mixing of the rows, an anisotropic lattice count and a conditional divisor estimate control the remaining small nonzero determinants, while a second congruence condition at an independent prime $q$, which places the residues on a cap of an affine quadric with no three collinear points, randomly shifted and linearly transformed and combined with the first condition by the Chinese remainder theorem, handles determinant zero together with a count over primitive null vectors; a deletion step followed by projective normalization to the unit square gives the point set, first for an unbounded sequence of sizes and then, by an elementary prime-interval estimate and monotonicity under deletion, for every sufficiently large $n$.

The problem page of Problem 507 asks for $\alpha(n)$, the same quantity for $n$ points in the unit disk. A translate of the unit square lies inside the disk of radius one, since the square's half-diagonal is $\sqrt2/2<1$, and translation preserves areas, so $\alpha(n)\ge\Delta(n)\ge c_1n^{-2+\eta}$ for every $n\ge n_0$. If the disk were read as having area one, scaling the square by $\sqrt{2/\pi}$ would place it inside and multiply every area by $2/\pi$, which changes the constant and not the exponent. In the other direction the disk of radius one lies in a square of side two, so $\alpha(n)\le4\Delta(n)$ and the two quantities have the same order; the upper bounds recorded on the problem page are not touched by this claim. The paper also names defects it finds in two earlier arXiv preprints that assert stronger power bounds for the disk's quantity $\alpha(n)$ itself, recorded on Ellmann's and Agama's claim pages.

Covers. The lower bound $\alpha(n)\ge c_1n^{-2+\eta}$ for an absolute $\eta>0$ and every sufficiently large $n$, through the transfer from the square to the disk stated above, and the consequence that no bound of the form $\alpha(n)\le C_\varepsilon n^{-2+\varepsilon}$ holds for every $\varepsilon>0$. No upper bound is claimed, and the estimate of $\alpha(n)$ asked for is open as before: the recorded bounds leave the exponent anywhere between $-2+\eta$ and $-7/6$. In the formal-conjectures statement file for the problem, at its commit of 2026-10-07 (507.lean), the bound for every large $n$ would answer the open variant erdos_507.lower, a function $\mathrm{ans}$ with $(\log n)/n^2=o(\mathrm{ans}(n))$ and $\mathrm{ans}\ll\alpha$, and neither erdos_507.equivalent nor erdos_507.upper; the Lean sequence form below would not answer it.

Depends on. No page of this wiki.

Formalization. The release's Lean development, the lean/ folder at the pinned revision linked above, states a weaker form of the theorem in OAI/Geometry/HeilbronnTriangle/Main.lean, with its definitions in Definitions.lean of the same folder. Points are pairs of reals, triangleArea is half the absolute value of the two-by-two determinant, pointsInUnitSquare is membership in the closed unit square, and triangleAreasAtLeast P a says that every triple of distinct points of the finite set P spans area at least a. OAI.Problem355.heilbronn_power_lower_bound proves that heilbronnExponent is positive and that there are a sequence of sizes n j tending to infinity and sets P j of exactly n j points, at least three, in the unit square with every triangle of area at least (n j) ^ (-2 + heilbronnExponent). OAI.Problem355.almost_n_minus_two_refuted proves that half that exponent is positive and that eventualAlmostUpperBound (heilbronnExponent / 2) fails, where eventualAlmostUpperBound ε says that for some C > 0 every large enough set of n points in the unit square has a triangle of area at most C * n ^ (-2 + ε). The exponent is fixed as 1 / (100000 * K) with K = T ^ 2 + 1, T the number of three-element subsets of an M-element set and M the binomial coefficient of 163 over 41, an extremely small positive number. The namespace Problem355 is the release's internal label and does not refer to another catalog problem. The Lean statement differs from the paper's Theorem 1.1 in two ways that this page records: it gives the lower bound along an unbounded sequence of sizes rather than for every large $n$, as the release's own scope note says, and it works in the unit square, so the transfer to the disk above is not in Lean. The comparator challenge lean/ComparatorChallenges/HeilbronnTriangle.lean pins both declarations with their definitions. This corpus's verification built both declarations at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked their axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the fingerprint of each was found identical to the challenge. Compared clause by clause with this page, the two statements certify the sequence form in the unit square and the refutation there of the almost-$n^{-2}$ formulation, which is exactly what the sequence form proves. They do not certify the bound for every large $n$, which rests on the manuscript's prime-interval estimate and deletion step alone, or the transfer from the square to the disk, which is elementary but not in Lean, so no formalized evidence is listed and the claim is claimed.

Acceptance. None recorded. The release attributes its manuscripts to an unreleased internal OpenAI model and names no individual author, so the claimant is the organization; its README says that the manuscripts were produced by an internal OpenAI model and are at different stages of verification. The release is a preprint with no journal record or arXiv version, the library's card records the manuscript without reviewing it, no outside review of it is recorded, and the site's page labels the problem OPEN with the Komlós–Pintz–Szemerédi lower bound as the best known (page last edited 30 December 2025, proof-claims thread without a claim as of 6 October 2026).