#507: Heilbronn's triangle problem — OpenAI's claimed first power improvement over Komlós–Pintz–Szemerédi (every triangle ≥ c·n^(−2+η), η ≈ 3·10⁻²³⁶), its Lean replayed here and extended by us from a sequence of n to every large n; Formal Conjectures' open #507 lower-bound question and Green's problem 77 answered in Lean from it

The problem. Erdős problem #507 [Er61, p. 246; Er75f, p. 107] is Heilbronn's triangle problem. Let α(n) be the largest number such that some n points in the unit disk determine no triangle of area less than α(n). Estimate α(n). Collinear triples count as area 0. The live page, last edited 30 December 2025 and read on 22 October 2026, gives

(log n)/n² ≪ α(n) ≪ n^−7/6+o(1).

• The trivial bound is α(n) ≪ 1/n.
• Erdős's parabola modulo a prime, recorded in the appendix of Roth's 1951 paper, gives α(n) ≫ 1/n².
• Heilbronn had conjectured α(n) = O(1/n²). Komlós, Pintz and Szemerédi disproved that in 1982 with (log n)/n². That was the best proven lower bound before this release. The two earlier claims of a power gain, described below, do not hold up.
• The upper bound has moved: Roth (1951, o(1/n)), Schmidt, Roth again, KPS 1981 (n^−8/7+ε), and Cohen, Pohoata and Zakharov (n^{−8/7−1/2000} in 2023, then n^−7/6+ε).

The common belief, as Zakharov's 2026 survey reports it, was that the truth sits at n^−2+o(1), that is α(n) ≤ C_εn^−2+ε for every ε > 0. The page carries no proof claims and no comments, and it does not mention OpenAI.

The claim. OpenAI, "A power improvement in the Heilbronn triangle lower bound" (dated 25 September 2026, 24 pages, public since 6 October as family 191 of github.com/openai/math). Theorem 1.1: there are absolute constants η, c₁ > 0 and an n₀ such that for every n ≥ n₀ some n points in the unit square have every triangle of area at least c₁n^−2+η. The unit square and the unit disk change α(n) only by a constant factor. If the theorem holds, the almost-n⁻² belief is false: α(n) ≥ n^−2+η/2 for all large n.

The exponent is explicit and extremely small. With d = 41, M = C(163, 41), T = C(M, 3) and k = T²+1 (§3), the paper's §8 gives η = 2/κ, where κ = 45435k+16 is the growth exponent of (8.6) and η is (8.7). Here M has 39 digits, T has 116 and k has 232, so η ≈ 3.18·10⁻²³⁶. The result is qualitative: it moves the exponent, not any number anyone will compute with.

Where things stand: OpenAI's own Lean proves a sequence form of the theorem, which already refutes the almost-n⁻² bound. Our Lean, built on theirs, proves the every-n form. No human has refereed the paper.

The construction. It is a random construction with arithmetic built in, not a hypergraph argument. KPS needed a hypergraph independence lemma for their log; this proof needs only plain deletion.

• Points from integer columns. A column u = (u₁, u₂, u₃) with 0 ≤ u₁, u₂ < N and N ≤ u₃ < 2N gives the point (u₁/u₃, u₂/u₃). Three columns forming a matrix A give a triangle of area |det A|/(2A₃₁A₃₂A₃₃). So small triangles are small determinants.
• A label that forbids small determinants (§3). Each column carries a random label ξ in the field F_r⁴¹. Columns (1, ξ, ξ²) with distinct labels have a nonzero Vandermonde determinant. The field norm of that determinant is a polynomial over F_r, and Lemma 3.1 writes it as a sum of T monomial 3×3 determinants.
  • The digit construction (3.6)–(3.8) puts the factors of each of those T determinants at designated base-B digit positions of the three rows. The positions are chosen by (3.7) so that only matched positions add up to k−1. So, modulo r, the coefficient of B^k−1 in the determinant's base-B expansion is the norm.
  • Lemma 3.3 shows that the coefficients are too small for carries to cancel it. Three distinct labels therefore force every integer representative of the determinant modulo h = B^k to exceed τ ≈ B^k−1/2 in absolute value.
• Mixing (§4). A random matrix in SL₃(ℤ/h) makes the residue matrix uniform on an orbit, and Lemma 4.2 bounds the orbit's size from below. The integral lifts have rows in a lattice of known index. The lattice counts of §2 then bound the number of lifts with any fixed nonzero determinant.
• Determinant zero (§§5, 7). Collinear triples need a second prime q ≈ h¹⁰⁰. Residues are taken from an elliptic-quadric cap (no three points on a line), with a restricted random translation that excludes short integer relations. Determinant-zero triples are counted by their primitive integer null vector, in three cases: affinely independent residues, and two cases with an equal pair of residues.
• Deletion (§8). A bad triple needs two equal labels. That has probability about r⁻⁴¹, which beats the factor h·D lost in the lattice count (D a divisor from the residue matrix's Smith form, of bounded mean). Sampling 2n_r columns and deleting one point per bad pair or triple leaves n_r points, with A_kr^κ ≤ n_r ≤ D_kr^κ and n_r²Δ ≥ r²/64. For every large n, a prime r ∈ (m, 2m] from Bertrand's postulate (with m = ⌈(n/A_k)^1/κ⌉) gives n ≤ n_r ≤ C_kn. Keeping any n of the points finishes the proof.

The Lean, and our replay. OpenAI's comparator challenge, ComparatorChallenges/HeilbronnTriangle.lean, states two theorems in namespace OAI.Problem355, which is OpenAI's internal label, not an Erdős number. (Comparator is the tool that checks that a solution proves exactly the challenge's statements, from the allowed axioms.)

• heilbronn_power_lower_bound: 0 < η and there are n_j → ∞ and n_j-point sets in the unit square with every triangle ≥ n_j^−2+η, for η = 1/(100000k).
• almost_n_minus_two_refuted: the almost-n⁻² upper bound fails at ε = η/2.

Both are weaker than the paper's Theorem 1.1: an unbounded sequence of n rather than every large n, and a smaller exponent, 1/(100000k) ≈ 7.2·10⁻²³⁷. OpenAI's scope note says so: "the paper's statement for every sufficiently large n is broader". The solution, OAI.Geometry.HeilbronnTriangle.Main, is 195 modules and 24,275 lines, and it imports nothing but Mathlib.

We compiled all 195 from source on our machine with Lean v4.34.1 and Mathlib d13f23b7, the repository's pins. We built module by module, with no cache for anything but Mathlib, three at a time: 195 of 195, 0 errors, 11 minutes of wall time.

• #print axioms under --trust=0 gives exactly propext, Classical.choice and Quot.sound for both theorems.
• We printed both theorems and the twelve definitions they use fully elaborated, every implicit argument shown (Lean's pp.all). Thirteen of the fourteen match the comparator character for character, after collapsing whitespace.
• The fourteenth, heilbronnK, differs by one attribute. OpenAI's Definitions.lean marks it @[irreducible]; the challenge does not. A probe of the kernel's own records shows the same definition on both sides: the same reducibility hint, the same value hash and type hash, both safe. The attribute only stops the elaborator from unfolding k. It changes no statement.
• A mutation test of the matching script caught all eight mutants: T² + 2 in place of T² + 1 in k, a changed kernel value hash, the kernel hint flipped to opaque, d = 43 in place of 41, the absolute value in the area replaced by a negation, an added axiom, a missing probe log and a missing block.
• A planted sorry surfaces as sorryAx.
• We scanned all 196 files for sorry, axiom, native_decide, implemented_by, extern, unsafe, opaque, admit, debug options and set_option. The only hits are the challenge's own two sorrys; there is not one set_option in the closure.

A second check, leanchecker --fresh, covered the whole environment: Mathlib, OpenAI's 195 modules and our three files (below). It re-checks every declaration from the stored terms through the kernel, independently of the build's elaboration, and it re-checks Mathlib's cached files too, which --trust=0 does not. It exited 0 after 3,516 s, with a peak of 8.2 GiB. A control naming a module that does not exist exits 1.

We were not first. Three third-party replays ran OpenAI's Comparator on this challenge before us. Two of them also noted that the Lean states less than the paper:

• mathvet/mathvet, 8 October, with Lean's kernel. Its fidelity table calls family 191 "weaker-statement".
• carlostoledo1891/cert-machine (run 38019899278, committed 10 October). Lean's kernel and the independent nanoda kernel both accept; its reading labels 191 "NARROWER — DECLARED".
• nealmcb/openai-math-lean-tooling. Comparator accepted it on 11 October, and both kernels accepted it again on 15 October.

Ours is a fourth, independent replay. It repeats the statement and definition match by a second method: pp.all text plus a probe of the kernel's records, which clears the one attribute difference that a kernel-level comparison does not see. It adds a scan of the whole closure. One module in OpenAI's folder, MainDigitBadTripleBound.lean, fails in the pinned nanoda according to nealmcb's report. It is not in the closure of Main.lean (our closure has 195 of the folder's 242 files), so it does not bear on either theorem.

Every large n, in Lean (ours). OpenAI's per-prime construction proves more than its comparator states. Its PrimeParameterData keeps both sides of its two Bertrand windows: 100k²r³⁰ < B ≤ 200k²r³⁰ and h¹⁰⁰ < q ≤ 2h¹⁰⁰. That is exactly what the paper's §8 interpolation needs, and it is what our file EveryN507.lean uses to prove Theorem 1.1 as the paper states it. The theorem is OAI.Problem355.EveryN.every_large_n: there are c > 0 and n₀ such that every n ≥ n₀ has n points in the unit square with every triangle ≥ c·n^−2+2/κ, κ = 45435k+16. That is the paper's own exponent η = 2/κ (8.7). The steps:

• The single-prime statement. We extracted it from the proof in OpenAI's Main.lean: same point law, same constants. For every prime r past a threshold, and every choice of parameters, there is a set of exactly ⌊a_r⌋ points, a_r = r√(N³/τ), with every triangle ≥ τ/(16N³).
• Two-sided growth. a_r² = r²(hq)³⁰/τ. The windows give h¹⁰¹ ≤ hq ≤ 2h¹⁰¹, B^k−1/3 ≤ τ ≤ B^k−1/2 and r³⁰ < B ≤ 200k²r³⁰. So r^κ ≤ a_r ≤ √C₀·r^κ with C₀ = 3·2³⁰·(200k²)^3029k+1. We proved these as inequalities between natural numbers first, with no division.
• Interpolation. Take the least m with n ≤ m^κ, and a prime r with m < r ≤ 2m (Mathlib's Bertrand). Then the construction at r has at least r^κ ≥ n points; keep any n of them. Its triangle bound is r²/(16a_r²). Since a_r ≤ √C₀·4^κ·n and r² ≥ n^2/κ, that bound is at least c·n^−2+2/κ.
• The corollary. every_large_n_heilbronnExponent gives the same with OpenAI's smaller exponent 1/(100000k).

All four theorems depend only on propext, Classical.choice and Quot.sound (axiom prints under --trust=0). Our n₀ is at least (400k²)^κ, a number with about 3·10²³⁸ digits. The paper's n₀ is not computed either.

An engineering note for anyone extending this. A single push_cast on the cast of 45435k+16, with the concrete k, ran past our 10 GB memory cap within a minute, although k is @[irreducible] in OpenAI's Definitions.lean. What worked was proving every arithmetic fact about k for a variable K and only then instantiating; the interpolation is proved for a general k the same way.

Formal Conjectures' #507 lower-bound statements, proved in Lean (ours). Formal Conjectures states Erdős #507 in its own vocabulary: points in the closed unit disk of ℝ², area through the plane's orientation form, α(n) as a supremum over non-collinear n-sets, and ≪ as big-O at infinity. Three of its statements concern the lower bound:

• erdos_507.lower, tagged research open: find an answer f with lowerBest = o(f) and f ≪ α, where lowerBest(n) = (log n)/n² is KPS's bound. FC leaves the answer sorry.
• erdos_507.variants.lower_kps82 (lowerBest ≪ α), tagged research solved, proof sorry.
• erdos_507.variants.lower_erdos (α ≫ 1/n²), tagged research solved, proof sorry.

Our file Bridge507.lean copies FC's definitions verbatim (docstrings and attributes stripped): ℝ²'s orientation instance, triangle_area with FC's own determinant lemma and its proof, the ≪/≫ notation, minTriangleArea, α and lowerBest. It supplies the answer n ↦ n^−2+2/κ (κ = 45435k+16, the growth exponent above) and proves all three statements verbatim from every_large_n:

• OpenAI's square is moved by (−½, −½) into the disk of radius 1/√2. That changes no area.
• The absolute value of FC's oriented area of the moved points equals OpenAI's area formula.
• A positive triangle makes the set non-collinear, through Mathlib's collinear_iff_of_mem and the alternating area form.
• The supremum is bounded, because every triangle in the unit disk has area at most 4.
• log n = o(n^2/κ) gives the little-o.

Each of the three depends only on propext, Classical.choice and Quot.sound. The controls:

• A script checks all 20 copied blocks against FC at 3bf943f1, and two mutated copies fail it.
• A planted sorry surfaces as sorryAx.
• Two stronger statements fail to compile with the same proofs, so the proofs are not passing vacuously: α ≫ 1/n, which is false because α ≪ n^−7/6+o(1); and the answer n^−2+4/κ, which is not proved here (it is probably true).

So FC's open lower-bound question now has a kernel-checked answer, and its two "solved" variants have proofs. The mathematics is OpenAI's; KPS's theorem is recovered here as a corollary of a much stronger one, not reproved.

The reading. I read the whole paper (eight sections and Appendix A) before briefing anyone. Then three seats read the mathematics and a fourth read the sources, all Claude Opus 5.5 (the served-model receipts are in the bundle). Each was briefed to refute, to quote the sentence it objected to by printed section and lemma number, and to grade every objection FATAL, GAP, ERROR or EXPOSITION:

• seat R1: §§2–4 and §6;
• seat R2: §5, §7, §8 and Appendix A;
• seat C: the finite lemmas by exact computation on scaled-down instances, each check with a mutation that must fail;
• seat W: the sources and the world (below).

A fifth seat read this page blind against the files. No seat found a FATAL error or a gap. R1 and R2 returned HOLDS AS READ, with only expository notes. C returned HOLDS AS READ on every finite claim it tested. Each check had a mutation that the checker rejected. That covers the finite lemmas, not the asymptotic constants. The blind reader returned SHIP AFTER FIXES: six must-fix and sixteen should-fix findings, all applied on this page. Among them: the norm sits in one coefficient of the determinant, not in one digit of the coordinates; one of our "false" control statements is probably true; and only two of the three earlier replays had noted the narrower Lean statement.

• The lattice counts (§2, R1).
  • Lemma 2.4's hard case (the third column reaches only one direction of its plane) checks step by step: the bound of order U⁴Z² normals per dyadic group, |y| ≍ UZ, and the fact that every eligible column lies on the one shortest line. The constant is uniform in the determinant t and the radii.
  • A brute-force count over 22 radius triples, up to (40, 3, 1) and (14, 14, 1), keeps count/(R₁R₂R₃)² between 85 and 275.
  • Proposition 2.5's Cramer bound uses ∏λ_i ≤ 3^3/2I ≤ 3^3/2|det V|, the right direction, though the paper never displays the chain (exposition).
• The digit obstruction (§3, R1).
  • The norm polynomial has coefficients in F_r. Its repeated-index coefficients vanish because r is odd, and the S₃ sign rule gives the T-term determinant decomposition without dividing by 3!.
  • R1 computed the norm polynomial exactly for d = 3 at r = 3 and r = 5 (179,910 and 241,122 terms) and confirmed Lemma 3.1's decomposition.
  • R1 also drew 2,100 random digit matrices on small cases (the paper's positions, its bound on B, arbitrary prescribed residues). Every one whose planted coefficient was nonzero mod r kept every representative of its determinant at least 1.9995·τ from zero.
• The orbits (§4, R1).
  • Full SL₃ orbit enumeration over ℤ/4, ℤ/8, ℤ/9 and ℤ/25 matches |SL₃|/|stabiliser| exactly, and the bound (21/64)h⁸/(D³E²) holds with margin at least 2, including the singular case e = k.
  • Lemma 4.3's tail bound (r/L)^4j is attained with equality in one exhaustive small case (B = 7, r = 3, L = 6), so (4.5) has no slack; no case violated it. The paper's conditioning pins exactly j base-B digits, because the digits lie in [0, B−1].
• The auxiliary cap (§5, R2).
  • The quadric has no three collinear points for q = 3 to 13 (0 collinear triples among all of them).
  • An exhaustive computation over all of AGL₃(F₃) and all 27³ target triples confirms Proposition 5.3's three weight bounds (largest ratios to the stated bounds 0.75, 0.84 and 1.00) and its support statement. The control is to let the shift put 0 into V: the "no zero column" claim then fails 2,029 times, so the check can see a violation.
  • R2's notes: "increases the probability of any event by at most two" means a factor of two.
• Determinant zero (§7, R2).
  • The three cases (affinely independent residues; an equal pair with an extra row equation; an equal pair without one, split by rank mod q) are exhaustive over the support of the weight.
  • Every power-of-h-over-q estimate checks.
  • Lemma 7.3's moment, which carries the only non-pointwise bound on g(x), was computed exactly for 53 matrices over B ∈ {2, 3, 5}, every (b, e) pattern including the singular ones. There were 0 mismatches in the equivalence B^j | g(x) ⟺ Cx ≡ 0 mod B^j, and the normalised moment sits near 24.4 whatever B, b and e are.
  • R2's notes: Case 1 should cite the last sentence of Proposition 5.3 rather than Lemma 5.2, and the t = 0 hand-off should repeat that the rows lie in Λ.
• The deletion and the exponent (§8, R2 and C). Recomputed symbolically: the exponent of r in a_r is κ = 1 + 30β = 45435k + 16, so A_kr^κ ≤ n_r ≤ D_kr^κ as in (8.6). The error terms decay with exponents 16 − 27285k and 32 − d = −9 (which is why d = 41 > 32 is needed), and the two-sided bound on a_r holds in exact integers. Every "sufficiently large r" condition is r ≥ r₀(k), so the conditions are compatible, and the Bertrand interpolation gives n ≤ n_r ≤ C_kn. Appendix A's elementary Bertrand proof is right. Our Lean proof of the every-n step confirms the interpolation independently, though through OpenAI's Lean construction rather than the paper's §8 text.
• The digit obstruction, end to end (C).
  • C ran the full §3 digit construction at d = 1 (k = 2, L = r² in place of r¹⁰, B a prime with B − 1 ≥ 100k²L³) for r = 3, 5 and 7. Of 7,630 triples with distinct labels, none had a determinant with a representative in [−τ, τ].
  • Repeated labels do produce small determinants, and even a determinant ≡ 0 mod h (r = 3, labels (0, 2, 0)). So the paper's collision accounting is necessary, not decorative.
  • Moving one designated digit position breaks the coefficient identity on every distinct-label triple, and the obstruction itself five times. A base that is too small gives 89–394 counterexamples.
  • A synthetic version with T = 4 (k = 17) exercises the matching rule (3.7) with the paper's positions: 0 failures. Dropping the "+1" from ℓ_a breaks the identity 453–825 times per run.
  • At d = 3 over F_r³ (r = 3, 5, 7), the norm polynomial's full 165³ coefficient tensor lies in F_r, is antisymmetric and vanishes on repeated indices. The T-term determinant sum equals the norm at 180 of 180 points for each r. With d = 2 (even) the alternation fails, as it should.
• Orbits, cap and moment, recomputed independently (C).
  • Lemma 4.2 over ℤ/4 (all 4⁹ matrices), ℤ/8, ℤ/9, ℤ/25 and ℤ/27: the worst ratio |O_C|D³E²/h⁸ is 0.65625 against the claimed 21/64. Both natural misstatements, D²E² and the bound without the determinant-image factor, are violated.
  • Lemmas 5.1–5.2 hold exhaustively for the paper's own constants at q = 2003, 1,000,003, 4,000,037 and 9,000,011, and in denser stress tests. A disallowed shift, a shift putting 0 into V, or a split quadric each produces forbidden relations or rich lines.
  • Lemma 7.3's normalised moment Σg³/(R³I) stays near 24–26 for R ≥ h and reaches 2,048 for R < h, so the hypothesis R ≥ h is needed. The paper meets it in the affine case, as it says, because the restricted shift excludes every relation with |x| ≤ H = h². C's only suggestion is to say up front that this is what the auxiliary prime is for.
  • For §8, the two-sided bound on a_r held in 18 of 18 exact toy instances. With β = 1515k (forgetting τ) it fails in all 18.

The world. Seat W checked the record around the claim, with quotations and dates.

• The belief. Zakharov's 2026 survey "Small triangles" says that "many believe (including Szemerédi) that it is 'almost' true: Δ(N) ⩽ C_εN^−2+ε" (§3) and calls it "the conjectured Δ(N) ≲ N^−2+o(1)" (§6). Ben Green's open problem 77 asks the same thing as a question. The paper does not cite Green's list. Formal Conjectures states it as Green77.green_77, still open there. Our Extra507.lean proves its negation, from the every-n theorem through FC's own α. As a control, the same statement with exponent +2 in place of −2 is provable from α(n) ≤ 4, and we prove it. So FC's statement is false because α is large, not because of its form.
• Earlier power claims. The paper describes Ellmann accurately and Agama in part.
  • Ellmann's arXiv 1703.03297 v12 calls its own argument heuristic.
  • Agama's arXiv 2006.05269 v13 builds its points from a regular polygon plus its centre. W found the paper's objection to it correct only in part, and too weak. The centre gives a collinear triple only when the polygon has an even number of vertices. The real failure is that three consecutive vertices of a regular m-gon span area of order m⁻³, which W checked numerically, so the claimed bound fails for every large polygon.
• After the release. Two drafts claim much larger exponents by building on OpenAI's construction:
  • Ivan Blinov (littleBro/heilbronn-triangle-bounds, from 8 October), "conditional on the pinned manuscript's geometric estimates", up to η = 1/50,893,237;
  • Qiuyu Chen (19 October), η = 2/100,866,719, using Blinov's pieces.
  Neither has a complete Lean proof: Chen supplies none, and Blinov's Lean covers some of the finite and algebraic steps. Big O Speedrun's board lists both, and OpenAI's ≈ 3.18·10⁻²³⁶, as "Claimed". We have not checked either draft.
• Big O Speedrun's statement. On 19 October Joshua Cortez proposed a trusted Lean statement for that board in pull request #20, BigOSpeedrun.HeilbronnTriangle.Bound η. It landed on their main branch as commit 079ac7b4 on 21 October. It says: for every large n, n points with every triangle ≥ c·n^−2+η. Its own README notes that OpenAI's comparator theorem is weaker, a sequence of n only. Our Extra507.lean proves Bound at OpenAI's exponent 2/(45435k+16), statement copied verbatim and checked. Their record for the statement says it "proves no board record". Their gate does not yet take Heilbronn submissions, so nothing has been submitted.
• Citations. Cohen–Pohoata–Zakharov's two theorems (arXiv 2305.18253 Thm 1.1; arXiv 2409.07658 Thm 1.8, published in Inventiones), KPS 1982's §2 and Roth 1951's appendix say what the paper says they say.
• Silence. As of 22 October:
  • Formal Conjectures still marks erdos_507 open, and W's searches of its issues and pull requests found none mentioning OpenAI's proof.
  • The teorth database still lists #507 as open (status last updated 31 August 2025).
  • Bloom's 8 October post on the release lists 25 Erdős problems, and #507 is not among them.
  • W found no expert comment on erdosproblems.com, Tao's blog or Mathstodon, MathOverflow, Hacker News, Reddit or Quanta. X could not be checked (a bot wall).
• Our own pages were wrong in three ways, now fixed. The banner on our July report said "Bloom calls these claims", but #507 is not on Bloom's 8 October list. It stated α(n) ≥ n^−2+η without the constant, the threshold or the square. And it did not say that the Lean covers only a sequence of n. The Bloom sentence was wrong the same way on the banners for #142, #505 and #978, the other OpenAI families we matched ourselves; all four now say so.

What is ours, and what is not. The construction, the theorem and the exponent are OpenAI's. Ours:

• a fourth kernel replay, with a second-method statement match and the kernel probe that clears the heilbronnK attribute difference;
• the Lean proof of the paper's every-n Theorem 1.1, which OpenAI's Lean does not contain;
• Lean proofs of Formal Conjectures' three #507 lower-bound statements and of the negation of its green_77, and Big O Speedrun's Bound at OpenAI's exponent;
• the AI reading of the paper and the small-case computations.

No human has refereed the paper or our files. #507 itself, estimating α(n), stays open: if α(n) = n^−β+o(1), then β lies between 7/6 and 2 − 3.18·10⁻²³⁶, and whether α(n) has that form at all is open too. (Later on 22 October: two drafts claim exponents near 2·10⁻⁸ on this construction. We refereed them at /day/507-blinov-chen-heilbronn-exponent-refereed, where they hold as read.)