Bigger than 1/n²?

The claim, in plain words

Put n points in the unit square. Every three of them make a triangle, and one is the smallest; Heilbronn’s problem asks how large that smallest triangle can be made. Three points on a line make it zero. Purely random points do badly: in our simulations their smallest triangle shrinks roughly like 1/n³. Erdős’s finite-field parabola reaches 1/n² (in our check, the smallest triangle of the p-point parabola is exactly 1/(2p²) for every prime p from 5 to 97), and so does sampling random points and deleting one point from each tiny triangle.

As the paper tells it, Heilbronn’s original conjecture asked whether the answer is O(1/n²); Komlós, Pintz and Szemerédi disproved it in 1982, reaching (log n)/n² with a hypergraph argument. On the upper side, Roth proved the first o(1/n) bound, refined by Schmidt and Roth; Komlós, Pintz and Szemerédi reached n^−8/7+ε, and Cohen, Pohoata and Zakharov n^−7/6+ε. The paper refutes “the almost n⁻² formulation, discussed in Zakharov’s survey”: that for every ε > 0 the answer is at most C_ε n^−2+ε. It attributes that formulation to no one. It also notes that earlier preprints by Ellmann and Agama claim stronger lower bounds, finds unresolved issues in the versions it cites, and says its objections concern the arguments, not the bounds themselves.

Result 191 is one OpenAI preprint, A power improvement in the Heilbronn triangle lower bound (24 pages, dated September 25, 2026). Its Theorem 1.1: there are absolute constants η, c₁ > 0 and n₀ such that Δ(n) ≥ c₁ n^−2+η for every n ≥ n₀. The paper gives an explicit η = 2/(45435k + 16), where k = C(M,3)² + 1 and M = C(163,41); by our arithmetic k has 232 digits and η is about 3 × 10⁻²³⁶. The paper calls it “fixed but extremely small”.

What it doesn’t claim

An explicit point set: the points are sampled at random and pruned, so the proof shows that good sets exist without writing one down. The constant c₁ and the starting size are not given. The gain is only in the exponent: by our arithmetic, n^η reaches 2 only when n has about 10²³⁵ digits, and for any n anyone could write down, the old log n factor is larger. Nothing new about the upper bound or the true answer; the gap runs from n^−2+η to n^−7/6+ε. No verdict on the earlier preprints’ bounds.

Where it stands

Posted as a preprint

OpenAI, 24 pages, dated September 25, 2026

Peer reviewed

Not yet

Checked in Lean

The refutation of the almost n⁻² bound, with a weaker lower bound, formalized by OpenAI; not run by us

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization: the comparator statements use the paper’s definitions of triangle area and of the almost n⁻² bound and refute that bound. Their lower bound is weaker than Theorem 1.1, but enough for the refutation: it holds along an infinite sequence of sizes rather than for every large n, with an exponent 4.4 times smaller, though with no constant in front. By our count the proof takes 195 files and about 24,000 lines, excluding Mathlib (source). We found no unproved steps by search; we have not rebuilt the proof. The collection’s formalization.yaml does not list this result. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

1. Areas as determinants. A point is a vector of three whole numbers (u₁, u₂, u₃), plotted at (u₁/u₃, u₂/u₃). A triangle’s area is a 3-by-3 determinant divided by twice the product of the third coordinates; with third coordinates between N and 2N, a big determinant means a big triangle.
2. Hidden labels. Every point gets a random label ξ from a finite field with r⁴¹ elements. The vectors (1, ξ, ξ²), the finite-field parabola behind Erdős’s construction, have nonzero determinant when the three labels differ.
3. One designated coefficient. Coordinates are written in a huge base B with small digits whose remainders are set by the label. The lower terms are too small to cancel one designated coefficient of the determinant, which equals, modulo r, the field norm of the label determinant: so for distinct labels every representative of the determinant modulo B^k exceeds half of B^k−1 in absolute value (Lemma 3.3). A shared random matrix of determinant one mixes the rows, and the columns are lifted to whole numbers in a big box.
4. Rare bad triples, and a second lock. Labels collide with chance at most 3/r⁴¹, and lattice counting makes any fixed nonzero determinant unlikely. Collinear triples (determinant zero) are handled by a second prime, with residues from a quadric surface with no three points on a line, joined by the Chinese remainder theorem.
5. Sample and delete. Sample twice as many points as needed and delete one from each bad pair or triple. Every remaining triangle has area at least τ/(16N³), so n²Δ ≥ r²/64; since n grows like r^α, r² is about n^2/α = n^η. No hypergraph lemma is needed; primes in every doubling range fill in every large n.

The numbers in the video

• Random points (ours): the median smallest triangle times n³ stays between about 0.2 and 0.8 for n = 10 to 320, while n² times it falls from 0.07 to 0.001 (Jiang, Li and Vitányi proved the n⁻³ order).
• Erdős’s parabola (ours): points (x, x² mod p)/p; the smallest triangle is exactly 1/(2p²) for every prime p from 5 to 97 (for p = 17, area 1/578).
• Deletion at the n⁻² scale (ours): from 40 random points, the triangles below 0.05/n² are removed by deleting a few points, leaving 20 points with n²Δ at least 0.05.
• The toy of the determinant obstruction with labels in the field of r elements (ours, not the paper’s parameters): every one of about 29,000 random triples with distinct labels had a large determinant; small ones appeared only with a repeated label.
• The digit count of k, η ≈ 3 × 10⁻²³⁶, the 10²³⁵-digit threshold and the Lean exponent ratio 4.4 are our arithmetic from the paper’s formulas. The Lean count is our count of the import closure.

Read the source

• A power improvement in the Heilbronn triangle lower bound (PDF), 24 pages.
• The Lean scope note.
• The collection’s catalog, where this is result 191.

The paper

OpenAI groups related papers into one result; this one has a single paper.

• A power improvement in the Heilbronn triangle lower bound

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.