#507: Heilbronn's triangle problem — the two claimed improvements of OpenAI's exponent (Blinov: η = 1/50,893,237; Chen: η = 2/100,866,719) hold as read by two AI referee seats, and the same argument gives η = 2/50,395,469 ≈ 3.97·10⁻⁸ (ours, under the same conditions, read by one further seat)

The problem. Erdős problem #507 is Heilbronn's triangle problem: how large can the smallest triangle among n points in the unit square (or disk) be made? Komlós, Pintz and Szemerédi's (log n)/n² from 1982 stood as the best lower bound until 6 October 2026. Then OpenAI claimed the first power gain, every triangle ≥ c·n^−2+η with η = 2/(45435k+16) ≈ 3.18·10⁻²³⁶. We refereed that paper and replayed its Lean earlier today: /day/507-openai-heilbronn-power-lower-bound-refereed.

Since then, two public drafts have claimed far larger exponents from the same construction. Big O Speedrun lists both on its Heilbronn board, together with seven earlier checkpoints of one of them, under the line "These results are Claimed: their authors published them, and we have not checked them." We found no one else who has checked either one (see "The world", below, which also lists what we could not read). This entry is that check.

The two claims.

• Ivan Blinov (GitHub littleBro), "Heilbronn triangle bounds: finite packings and improved scales", a "conditional research draft … extending OpenAI math family 191, with OpenAI Codex assistance". His current claim is η = 2/(249k+5) = 1/50,893,237 ≈ 1.96·10⁻⁸ with k = 408,781, for every sufficiently large n. It is the head of an open, unmerged pull request (#13, commit e29a291, 15 October). His main branch carries the previous checkpoint, 1/145,278,430. He calls it "conditional on the pinned manuscript's geometric estimates and the written transfer". That means: it reuses OpenAI's §§2–8 and changes parameters, and the changes are a written diff against OpenAI's TeX. His Lean covers the new finite algebra and a finite probability theorem, not the geometric argument.
• Qiuyu Chen, "A smaller lift box in the degree-five Heilbronn construction" (PDF dated 18 October, released 19 October; the PDF carries no author line, and the repository credits "Euler, a mathematical research system", whose README names "Astra and GPT-6.1 Sol"). It keeps Blinov's construction, shrinks the lift box, and reproves the geometric estimates with explicit constants: η = 2/100,866,719 ≈ 1.98·10⁻⁸, c = 2^{−10,086,671,700}, for every n ≥ 2^{100,866,718·250}. That is 0.9% above Blinov. No Lean.

Neither draft has a human referee. Blinov's is not a self-contained paper: it is a patch to OpenAI's. Chen's is a 12-page paper. It credits Blinov's checkpoint for the algebra and the collision lemma and restates their proofs in compressed form (its §2), and it proves the geometric estimates afresh with explicit constants (§§3–4). So "is it true?" splits into three parts: is OpenAI's argument right (our earlier entry: holds as read, no human referee); does the transfer to the new parameters hold (this entry); and is the new collision lemma right (this entry).

Where the exponent comes from. OpenAI's construction samples about n_r ≈ r·(N³/τ)^1/2 integer columns in a box of side N, deletes one point from every small triangle, and keeps every triangle ≥ τ/(16N³). So n_r²·Δ ≈ r², and if n_r ≈ r^κ the gain is η = 2/κ. (It is η = 2γ/κ when, as below, the deletion only closes with r^γ in place of r, so that n_r²·Δ ≈ r^2γ.) Here r is the prime that labels the points, B (a fixed power of r, up to constants) is the digit base, h = B^k, q is a second prime, and N is a power of hq. Three things set κ, and they multiply:

• The digit base. OpenAI: B ≈ r³⁰. Blinov: B ≈ r⁶. Blinov makes the first two digit rows deterministic given the label (digit range r, one choice per residue) and keeps all the randomness in the third row (range about 400k²r⁴).
• The box. OpenAI: q ≈ h¹⁰⁰, N = (hq)¹⁰. Blinov: q ≈ h⁶, N = (hq)⁴. This is made possible by a "slab" cap, {(x, y, x²−νy²) : 0 ≤ x < w}, in place of OpenAI's cap cut out by the cube {0..w−1}³, together with H = 2h in place of OpenAI's H = h². OpenAI's short-relation argument only ever uses the first coordinate. Chen: N = (hq)⁴/B¹⁰²¹⁹⁵.
• The number of digits, k. OpenAI: d = 41, k = C(C(163,41),3)²+1, a 232-digit number. Blinov: d = 5, and the field norm written as 2,916 determinants instead of C(C(19,5),3). He uses the Conner–Gesmundo–Landsberg–Ventura Waring decomposition of the 3×3 determinant (18 cubes), restated as an identity 3·det A·det C = Σ_t=1¹⁸ Π_j h_t(A_·j, C_·j), plus nine-node interpolation. He then places the 2,916 determinants at digit positions from the base-3 {0,1} words, a set with no three-term arithmetic progression (Erdős–Turán 1936). That gives k = 2·204,390+1 = 408,781.

The price of B ≈ r⁶ is the collision bound. With d = 5, two equal labels have probability about r⁻⁵, against a loss of about B ≈ r⁶ in the lattice count, and OpenAI's deletion no longer works. Blinov's new lemma (orb:tagged-moment in his patch) restores it. With two equal labels the determinant polynomial factors as U(Y)(Z₁(Y) − Z₂(Y)). Here U comes from the deterministic top rows. "Tags" are the label's coordinates, written into the lowest digit positions of row 2, and they make U's first nonzero coefficient sit at a small known position a. A small determinant needs the coefficient of Y^k−1 to vanish, and that coefficient is linear, with slope −U_a ≠ 0, in one fresh third-row digit at position k−1−a. That digit lies outside every low digit that controls the Smith divisor. So a small determinant costs an extra factor 1/M, with M ≈ 400k²r³. The total collision moment becomes 6/(Mr⁵) + 2/r¹⁰ = O(r⁻⁸), and the deletion closes with r^γ in place of r, γ = ρ/(ρ+1), ρ = 249k+3. That gives κ = ρ + γ and η = 2γ/κ = 2/(ρ+2).

The reading. I read OpenAI's paper again in full, then Blinov's patch, review guide and notes, and Chen's paper, before briefing anyone. Four seats followed, all Claude Opus 5.5 (the served-model receipts are in the bundle), each briefed to refute and to quote the sentence it objects to. Two of them, P and G, refereed the drafts:

• seat P: the algebra, the packing and the fresh-digit lemma (Blinov's §§3–4 hunks, Chen §2);
• seat G: the geometric transfer (Blinov's §§5–8 hunks, Chen §§3–4);
• seat W: the world, priority and credits;
• seat S: our own additions, below.

Verdict on both drafts: HOLDS AS READ, from the two referee seats. P and G found no gap and no wrong inequality. Their findings are notes, listed further down. Concretely:

• The 18-term identity (P). P parsed the table out of Blinov's patch and transcribed Chen's by eye from the rendered page; the two are identical. Then Σ Π h_t − 3·det A·det C reduces to zero in ℤ[u]/(u²−u+1), checked symbolically with all 18 matrix entries indeterminate. Every one of the 54 single sign flips breaks it, and so do multipliers 1, −3 and 6.
• The degree-five norm decomposition (P), end to end in real finite fields. P built F_37⁵ and F_43⁵ and followed the patch literally: conjugate pairs, the 18 forms, the factor 3⁻², the constant-coordinate functional and nine interpolation nodes, 2,916 determinants per input. The sum equals the field norm on 60 of 60 random inputs at each prime, and on Chen's arbitrary-basis variant. Distinct labels give a nonzero sum and two equal labels give zero. Dropping a node agrees on 1 of 20 inputs, chance level (about 1/r); omitting 3⁻² agrees 0/20; at r = 41 ≡ 2 (mod 3) the construction cannot be built.
• The packing (P), exhaustively. Exactly 5 base-3 {0,1} words below 10 and 2,921 below 204,391. All 4,267,581 pairs in the set are midpoint-free. The full position support has exactly 2,916 triples summing to k−1, all matched and tag-free. Moving one tag (tags 0, 1, 3, 4, 8 in place of 0, 1, 3, 4, 9) creates a spurious triple, (12, 8, 408,760).
• The fresh-digit lemma (P). P read it line by line: the factorisation, the low digits of rows 1–2, the carry bound, the conditioning, θ = B/M² ≤ 1/2 and the three-pattern sum. P then built its own exact toy models. One uses small bases with tags, label-dependent residues and three regimes for the third-row residues (label-dependent, all zero, shared), and computes the Smith exponent from all nine minors. The other uses a base B above 100k²P, with P = L₁L₂L₃ = 400k²r⁶ as the lemma requires, and the actual event "the determinant has a representative in [−τ, τ]". In both, every joint probability Pr(b ≥ j and the determinant is small) ≤ M^−(2j+1), and the bound is tight (1/243 = 1/243 at M = 3, j = 2). Three negative controls fail as they must: the fresh digit inside the low prefix (1/4 against a bound of 1/8), a fresh position v < j (1/64 against 1/128), and a missing distinguishing tag. On the real layout at r = 37, with distinct labels, the coefficient of B^k−1 is ≡ the field norm (mod r) in 4 of 4 cases, by brute force over all supported positions.
• The geometric transfer (G). G traced every use of each changed parameter through OpenAI's §§5–8:
  • The slab cap: its points lie on the anisotropic paraboloid, so no three are collinear. Only the first coordinate is used anywhere, and 0 is still outside the shifted set. Exhaustive toy checks pass, and three mutations fail.
  • H = 2h: the short-relation exclusion and Lemma zero:moment's R ≥ h.
  • q ≈ h⁶: the three determinant-zero cases come out ≤ 8000²h⁶/q, 8000h⁴/q and 8000²h⁶/q².
  • N = (hq)⁴: the pair term is r^γτ^−1/2.
  • The deletion and the exponent, by exact arithmetic: β = (83k+1)/2, κ = ρ + γ, η = 2/(249k+5) = 1/50,893,237.
• Chen (G). G checked his smaller box against every place N's size matters, and recomputed his explicit constants (B2)–(B19) and the transfer to every n. It also checked his prime-counting input against the current arXiv version of Bennett, Martin, O'Bryant and Rechnitzer: Theorem 1.2 with (1.10)–(1.11) gives, at q = 3 and x ≥ 8·10⁹, the constant 1/840, which implies the weaker 1/160 he uses, as he notes. G found no wrong inequality. η = 2/100,866,719, c = 2^{−10,086,671,700} and the threshold all check out.
• The arithmetic, by me, separately. Exact fractions reproduce both exponents and the counts 5 and 2,921.

The notes, none load-bearing:

• The 18-form table works only if (σ(1), σ(2), σ(3)) is read in one-line notation; read as σ⁻¹, the identity fails. Both drafts write h(x,y) = Σc_ix_σ(i)y_i, which fixes the reading. Blinov's patch does not say so; Chen's coefficient rule (a_j = p(b_j)) does.
• The patch's descent step uses notation (the coordinate polynomials x̂, the Lagrange elements c_s) that it never defines; the notes and Chen define it.
• "the equation F_k−1=0 determines that digit uniquely" should be "admits at most one of the M allowed values", which is what the proof uses. Chen says it correctly.
• Chen's §2.1 cites "the packet's checker". It is not a file in his repository; it ships inside the PDF, as the attachment mathematical-supplement.zip. That holds one file, checkers/check_exact_inputs.py, which implements the 486-term expansion his text describes and, in its own words, checks "exact arithmetic only; full construction and all-n transfer unproved". We read it and did not run it. (Seat P had looked only at the repository and first reported it missing; the blind reader found it.)
• Stale sentences that the patch does not touch: §1 still says "a sum of monomial determinants" and that Appendix A's Bertrand lemma is used for the interpolation (the patched §8 uses the prime number theorem for primes ≡ 1 mod 3).
• The review guide points the exponent identity at a theorem for the previous checkpoint's k.
• Chen's stated reason for the constant 4 in (B8) is loose. The constant itself holds (the true value is below 2.34).
• Chen's s₀ = 102,195 = (k−1)/4 is not forced. His own inequality allows every s₀ ≤ 136,259, which gives η = 2/(246k+17) = 2/100,560,143.

Blinov's Lean, replayed here. We compiled, from his source, the 48 of his modules that the theorems his review guide cites import (the degree-five norm decomposition, the polynomial coordinates and distinct-label criterion, the repeated-column factorisation, the tagged and total small-residue moments, column reindexing, the reserved-word packing and its exact counts). We built against Mathlib 20c73142's published build cache; Mathlib itself was not rebuilt, and --trust=0 does not re-check its cached files. Lean 4.11.0 and Mathlib 20c73142 are his pins. We built with our own driver, module by module, not with his build files: 48 of 48, 0 errors. #print axioms under --trust=0 gives propext, Classical.choice and Quot.sound for 16 of the 17 theorems, and no axioms at all for the seventeenth, the integer comparison gain_from_five. A planted sorry surfaces as sorryAx. Before building, we scanned all 99 files for sorry, admit, axiom, native_decide, implemented_by, unsafe and for code that runs at compile time (#eval, run_cmd, macros, IO); there is none. This confirms his finite theorems. It does not touch the geometric argument, which no one has formalized at these parameters.

Ours: the same argument goes further, to η = 2/50,395,469 ≈ 3.97·10⁻⁸. Twice Chen's exponent, by three changes. Every input the drafts rely on is unchanged, and so is their condition (OpenAI's argument as transferred by Blinov, refereed here, with no human referee). There is one new elementary lemma, and seat S was briefed to break all three changes. S returned HOLDS WITH FIXES, with no error found; its fixes are in the wording below.

1. A sharper bound for coinciding points (seat G). The pair term n_r·Pr(π(u)=π(v)) is the only constraint on the box besides the triple term. OpenAI's Lemma sam:proportional bounds that probability by a lift count that ignores the residues: ≪ (hq)⁶N⁻³. In Blinov's construction the residues give more:
   • If u and v are proportional over ℤ, all 2×2 minors of (u|v) vanish. Λ²G_h is invertible, so the minors of the digit columns vanish mod h. That fixes the second column's whole third row, whose k digits each have M equally likely values: probability ≤ M^−k.
   • Modulo q, the second residue must lie on the line through 0 and the first. That line meets the cap image V in at most two points: probability ≤ 2/s.
   • Given the shared choices the two are independent, so Pr(π(u)=π(v)) ≤ 2C·M^−ks⁻¹(hq)⁶N⁻³.
   That buys r^63k of room in the box. Toy enumerations confirm both steps, and three mutations that should break them do: a rank-one G, a digit range above B, and a non-cap set.
2. A better progression-free set (credit: J. Wróblewski). The matching property needs only that the digit positions have no three-term arithmetic progression: i + j + ℓ = k−1 becomes x + y = 2z. The tag argument needs three more things. The set contains 0, since row 1's tag sits at position 0 and is excluded only because 0 belongs to the set; shifting a good set by 1 breaks this, which S confirmed. The five tags are its five smallest elements, so all five lie below the first norm word T. Blinov's lemma then goes through with every "below 10" in his text read as "below T": the fresh digit sits at k−1−a > a, and θ ≤ 1/2 bounds the tail for any a. So any 3-AP-free set of 2,921 integers containing 0 works, with k = 2·max + 1. Wróblewski's table of non-averaging sets gives a(2921) ≤ 137,693, that is, a 2,921-element 3-AP-free set inside [1, 137,693]. It is built from the 216th roots of unity modulo the prime 3889, by his "Theorem 216". Seat W rebuilt it from that description, and seat S and I each rebuilt it again from his recipe (the 216th roots of unity mod 3889 under x ↦ 1331x + 640, in 14 blocks); all agree element for element. Two independent checkers find no three-term progression, and a planted one is caught. Shifted to start at 0, its smallest elements 0, 15, 16, 21, 22 are the tags and T = 37. Its k is 2·137,692+1 = 275,385, against 408,781. S enumerated every pair of designated positions in rows 1 and 2: exactly 2,916 position triples sum to k−1, all matched and none involving a tag. S also checked the tag minor on the real layout at r = 37, 20,000 label pairs with each first differing coordinate forced: U vanishes below a and 0 < |U_a| < r every time. Blinov's Lean certificates hard-code his set, so they do not cover this one; our scripts do. (Before W found Wróblewski's table we built a product of our own: 163·w + l, with w among the first 127 base-3 {0,1} words and l from a 23-element 3-AP-free set in [0,81] that our exact search found to be optimal. It reaches 178,077. It is AP-free because l + l′ ≤ 162 < 163 splits x + y = 2z into two such equations, and S checked it the same way. Wróblewski's is better.)
3. A smaller box. With step 1, take N = h·q·B^u. The pair term is then ≪ r^γB^{20.5k+0.5−1.5u}, which tends to 0 exactly when 3u ≥ 41k+2. The triple term depends on N only through (log N)². So n_r ≍ r^γ+X with X = 60k + 9u + 3, and with γ = X/(X+1), η = 2γ/(γ+X) = 2/(X+2). At k = 275,385: u = 3,763,596, X = 50,395,467, η = 2/50,395,469. S checked again every place N's size enters, at this smaller N: λ₃ ≤ 4N, the determinant-zero cases, the shell counts, log N = O(log r), and the two-sided bounds on n_r. S's script derives every exponent from the parameter definitions; my own only checked that my formulas agree with each other, which S rightly called circular. None of this is optimized. Any γ < 1 works, so η can be pushed toward 2/(X+1). A box with a power of r in it does marginally better. S also found a rigorous extra factor r⁻⁵ in step 1 (proportional points force equal labels), which gives 2/50,395,460. We state the version without it. With step 1's pair bound as stated above and the printed triple bound, the supremum over boxes and γ is 2/(183k+8) = 2/50,395,463 at this k, not attained; with the extra factor it is 2/(183k+3) = 2/50,395,458. It is not a ceiling of the construction: the binding loss is still the residue-blind lift count, and a count that used the residues would go further, which is not proved here.

The three steps one at a time, from Chen's 2/100,866,719 ≈ 1.98·10⁻⁸:

• Without step 1, a smaller box is exactly Chen's move. His own inequality allows it down to 2/(246k+17) = 2/100,560,143 at Blinov's k.
• Step 1 with step 3, Blinov's k: 2/74,806,940 ≈ 2.67·10⁻⁸.
• Step 2 alone in Blinov's formula: 2/(249·275,385+5) = 1/34,285,435 ≈ 2.92·10⁻⁸.
• All three: 2/50,395,469 ≈ 3.97·10⁻⁸.

Two things this is not. It is not a new method: the construction is OpenAI's, every step except step 1 is Blinov's or Chen's, the set in step 2 is Wróblewski's, and step 1 is a short observation about OpenAI's lemma in their setting. And it is not more certain than the drafts: it adds one lemma to the same conditional chain, read by one seat. We have not posted it to Big O Speedrun's board.

The world. Seat W looked for any check of either claim and found none:

• Blinov's repository has issues disabled, no forks, and no comment or review on any of its 13 pull requests.
• Chen's repository is one commit with no activity.
• Big O Speedrun's Heilbronn board has no posts; its verifier holds only the target statement (merged 21 October), and "no current board record has a complete Lean proof".
• erdosproblems.com/507 has no comments and no proof claims (comments are suspended) and does not mention OpenAI.
• Nothing on arXiv after 6 October, Hacker News, MathOverflow, Math.SE, Tao's blog or Wikipedia. X, Reddit, the BOS Discord and Chinese-language forums could not be read.
• OpenAI has not changed the family-191 preprint since 6 October; Blinov pins it at fd4aeeb, and its files are identical there and at the 1581d4c we refereed.

Credits, checked against the sources:

• The 18-term decomposition is Conner, Gesmundo, Landsberg and Ventura's Theorem 4.1 (arXiv 1909.04785 v2; Theorem 2.11 in v1): the Waring rank of det₃ is at most 18, over ℂ, with ϑ = e^2πi/6. The ring identity with the factor 3 is Blinov's restatement. Chen says so correctly ("Their theorem states a complex Waring decomposition").
• The slab cap is Blinov's, first in his commit of 8 October; we found no earlier source.
• The base-3 {0,1} set is Erdős and Turán's (1936, the footnote on p. 263).
• Big O Speedrun prints Chen's threshold as 2^{100866718·250}; the paper has 2^{100866718·250}.

If you are looking for a hole. Look first at the fresh-digit lemma's conditioning: the exact toys show its bound is tight, so there is no slack to hide an error, and putting the fresh digit inside the low prefix breaks it. Then look at step 1 of our own addition, the sharper pair bound: it is the newest piece here, and one seat besides its author has read it. Then look at OpenAI's §7, the determinant-zero count. Everything here rests on it, and no human has refereed it.

What is ours, and what is not. The construction is OpenAI's; d = 5, the tags, the fresh-digit lemma, the slab cap and the transfer are Blinov's; the smaller box and the explicit constants are Chen's. Ours: an independent reading of both drafts, the first we could find (two referee seats, P and G; the 18-term identity checked symbolically; the full norm decomposition checked in two real finite fields; the packing checked exhaustively at the real parameters; the fresh-digit lemma read line by line and tested on exhaustively enumerated toy models, with controls that fail); a replay of Blinov's finite Lean; the sharper pair bound (seat G); and its combination with Wróblewski's set and a smaller box, which gives η = 2/50,395,469 under the same conditions as the drafts. The set itself is Wróblewski's. No human has refereed OpenAI's paper, either draft, or our files. #507 itself, estimating α(n), stays open: if α(n) = n^−β+o(1), then β lies between 7/6 and 2 − 3.97·10⁻⁸ if everything above holds, and whether α(n) has that form at all is open too.