HorizonMath, a benchmark of 113 mostly unsolved problems, credits frontier models with six discoveries and prints the constructions for three. Decided here from what it prints: the Kakeya construction's area holds, exactly. The Ramsey certificate — a claimed improvement of the best upper bound on diagonal Ramsey numbers, from 3.7992 to 3.6961 — does not satisfy the theorem it is applied to: the checker that accepted it admits pairs of numbers the theorem's region cannot contain, and the certificate uses one at the point that sets the constant. The other three expressions are not published.
The paper: arXiv 2603.15617v2 (10 September 2026, CC BY 4.0), Appendix A; the benchmark's code at github.com/ewang26/HorizonMath @ 4ef0b61a; the theorem: Gupta, Ndiaye, Norin and Wei, arXiv 2407.19026v2. Each pinned by sha256 in corpus/horizonmath, the printed constructions transcribed there. What is refuted is a certificate, not an inequality: whether R(k,k) ≤ 3.6961^(k+o(k)) is true is untouched. Nothing has been sent to the authors.
Campos, Griffiths, Morris and Sahasrabudhe proved R(k, k) ≤ (4 − ε)^k in 2023; Gupta, Ndiaye, Norin and Wei (GNNW) optimised the argument to R(k, k) ≤ 3.7992^(k+o(k)). Their Theorem 14 turns three conditions on functions F, M and Y of λ = ℓ/k into the bound R(k, ℓ) ≤ e^(F(ℓ/k)k + o(k)): F and F′ positive; the pair (X(λ), Y(λ)) in a region R, with X(λ) = (1 − e^−F′(λ))^(1/(1−M(λ)))·(1 − M(λ)); and F(λ) > −½(log X + λ log M + λ log Y). At λ = 1 the bound is the diagonal one, c = e^F(1).
HorizonMath poses this as a problem and credits GPT-5.4 Pro with a certificate: GNNW's own cubic correction plus −0.0778 λ⁵, and M and Y constant on 200 intervals of (0.001, 1]. Its checker accepts it, with c = 3.69608391263. The rebuilt certificate reproduces that number here, enclosed: 3.69608391263329.
The paper calls this "a verified certificate in the Gupta–Ndiaye–Norin–Wei framework", and says all six discoveries "have been verified by domain experts".
GNNW define R through its interior points: pairs (x, y) with R(k, ℓ) ≤ x^−k y^−ℓ for all k and ℓ with k + ℓ large. A bound known for ℓ ≤ k, R(k, ℓ) ≤ e^(U(ℓ/k)k), places a pair in R when, for every s in (0, 1],
Their Lemma 15 proves both lines before it places a point. HorizonMath's statement defines its inner region by the first line alone and adds: "Since R(k, ℓ) = R(ℓ, k), the pair (x, y) is accepted if either (x, y) ∈ R₀ or (y, x) ∈ R₀." Symmetry makes R symmetric; it does not turn a one-sided test into a two-sided one. Because U increases on (0, 1], the first line holds for every y as soon as x ≤ e^−U(1) = 0.26292279 — so the rule accepts, for instance, (0.26, 0.9999), which R cannot contain.
Membership in R has a price that can be checked from below. For k, ℓ ≥ 3 and 0 < p < 1, colour the edges of K_N red with probability p, with N = ⌊min(p^−(k−1)/2, (1 − p)^−(ℓ−1)/2)⌋: the expected numbers of red K_k and blue K_ℓ are each below 1/6, so some colouring has neither, and R(k, ℓ) > N (Erdős 1947). If (x, y) were in R, then along k = ⌈eℓ⌉ the two bounds would force e·(−log x) + (−log y) ≥ min((e/2)(−log p), ½(−log(1 − p))), and the same with x and y exchanged.
At λ = 1 the certificate's pair fails that with e = 13/2000 and p = 11981/500000: the lower bound grows at 0.012127 per ℓ, the pair allows 0.010826. Both are enclosed in decimal intervals at 60 digits, every rounding outward. The pair is not in R; Theorem 14 does not apply; the certificate proves nothing about c.
| λ | X(λ) | Y(λ) | decided | witness |
|---|---|---|---|---|
| 0.0010 | 0.99769 | 0.26321 | OUTSIDE R | Erdős at e = 19/2000, p = 8033/250000: gap 0.00134 |
| 0.0058 | 0.98706 | 0.26601 | NOT PLACED | U(319/1000) exceeds -ln x - s ln y by 0.2406 |
| 0.0331 | 0.92892 | 0.28245 | NOT PLACED | U(703/2000) exceeds -ln x - s ln y by 0.2000 |
| 0.1407 | 0.73107 | 0.35746 | NOT PLACED | U(541/1000) exceeds -ln x - s ln y by 0.0632 |
| 0.3134 | 0.50087 | 0.52209 | NOT REFUTED | — |
| 0.5725 | 0.26328 | 0.99325 | NOT PLACED | U(157/500) exceeds -ln y - s ln x by 0.2436 |
| 0.8316 | 0.26070 | 0.99880 | OUTSIDE R | Erdős at e = 23/2500, p = 31483/1000000: gap 0.00234 |
| 1.0000 | 0.22745 | 0.99880 | OUTSIDE R | Erdős at e = 13/2000, p = 11981/500000: gap 0.00130 |
Across the certificate: 56 of 201 points outside R, each with its own (e, p); 128 where one rational s shows the problem's own U does not place the pair (it may or may not lie in R by some other bound); 17 not refuted — the pairs with X near the window where the xy = e^−U(1) branch is legitimate.
The checker, run as published at the pinned commit, accepts the certificate in 107 s. With min(bu, bs) changed to max(bu, bs) — both orientations required — it refuses it in 0.2 s, on the first interval: "R_0 check failed somewhere on [0.001, 0.0010014]".
128 thin triangles with slopes i/128, base width 1/128, and 128 intercepts the model chose — every one a multiple of 1/1024. Between two consecutive crossings of the 256 edge lines the union's cross-section has a fixed combinatorial shape, so its length is linear there; summing width times midpoint length over the 4,033 pieces gives the area as a rational, with no rounding anywhere:
That is 0.00566233 below the printed AlphaEvolve baseline 0.1148103258186177, and the paper's 0.1091479892 is its rounding. The benchmark's own checker computes the same area in floating point, to 15 digits, against Keich's older baseline.