Erdős Problem #507
Heilbronn's triangle problem

Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, Heilbronn: for every large n, some n points in the unit square have every triangle of area ≥ c·n^(−2+η), η = 2/(45435k+16) ≈ 3·10⁻²³⁶ — the first power gain over Komlós–Pintz–Szemerédi's (log n)/n² (1982); the estimate of α(n) stays open — read by AI referee seats here 22 Oct, see /day/507-openai-heilbronn-power-lower-bound-refereed — family 191 at github.com/openai/math, OpenAI's own Lean proves the sequence form only — for an unbounded sequence of n, n-point sets in the unit square with every triangle ≥ n^(−2+η), η = 1/(100000k), and the refutation of the almost-n⁻² bound at ε = η/2 (its scope note: "the paper's statement for every sufficiently large n is broader"). Kernel-replayed on our machine on 22 Oct 2026, after three earlier third-party Comparator replays (mathvet 8 Oct; carlostoledo1891/cert-machine 10 Oct, with nanoda; nealmcb 11 and 15 Oct): 195 modules importing only Mathlib, 0 errors, standard axioms, both theorems and twelve definitions matched to the comparator under pp.all (one differs only by an @[irreducible] attribute; the kernel's records agree). Our Lean extends it to the paper's Theorem 1.1 for every large n, with the paper's exponent 2/(45435k+16), and proves Formal Conjectures' erdos_507.lower, its two lower-bound variants and the negation of green_77 from it — see our /day entry. This problem is not among the 25 on Bloom's 8 Oct list of the release's Erdős claims; the match to family 191 is our own reading, not Bloom's.