Tao's optimization-constants registry has fifteen open pull requests, most of them machine-assisted, none reviewed since September. Five are read here from their submissions: two exact step functions that tighten the autocorrelation and minimum-overlap constants, a two-law entropy certificate for C₃c, five one-line bounds, OpenAI's nine-dimensional Borsuk counterexample, and a "certified record package" for the de Bruijn–Newman constant at 0.1595. Every finite object decides and holds; the proofs read hold; and the package, 104 files whose scorer compares rationals and hashes while its analysis cites a bank outside the bundle, is refused — not wrong, undecidable from what was submitted.
teorth/optimizationproblems at 2c1968cd (main; unchanged since 2026-09-26) and its open PRs #210, #217, #221, #225, #226 as fetched 2026-10-15, with the constructions they link (Atris records @ 1fa857a0, Zenodo 23289305, Mosaic's fork @ cc810785, OpenAI's BorsukNine through this repository's own kernel record), every byte pinned by sha256 in corpus/optconst-queue/PINS.json; the claimants' scorers kept as text and never run. Definitions are the registry's constants/*.md. Pre-registered in corpus/optconst-queue/preregistration.json. Two of #226's five bounds (16a, 70a) are not decided in this campaign and say so.
| PR | constant | claim | decided by | verdict |
|---|---|---|---|---|
| #225 | C_1a | C_1a <= 1.5027435 (an upper bound exhibited by an explicit 65,536-step function with exact rational heights; Atris records @ 1fa857a0) | the 65,536 heights as integers over one denominator; the autoconvolution computed as ONE exact integer product by Kronecker substitution and the maximum taken o… | CERTIFIED |
| #225 | C_1b | C_1b <= 0.38085856 (an upper bound exhibited by an explicit 114,688-step function with exact rational heights; Atris records @ 1fa857a0) | the 114,688 heights as integers over one denominator; the correlation with 1 - h computed as ONE exact integer product by Kronecker substitution and the maximum… | CERTIFIED |
| #221 | C_3c | C_3c >= 1.674894211307116 from two laws on 51 and 47 points of Z^2 (weights multiples of 10^-50) mixed in counts 39041372760532870645 : 60958627239467129355 of 10^20 b… | per-law pushforwards exact; entropies as directed-rounding intervals at 128 bits (instruments/sumdiff + bigfloat, no code of the claimant's); the mixture by rat… | CERTIFIED |
| #226 | C_20a | C_20a >= 8: X = E - 1 (E standard exponential) is isotropic log-concave with Var(X^2) = 8, and products of independent copies give Var(|X|^2) = 8n (Patankar) | E[E^k] = k! exactly; E[(E-1)^4] = 9, E[(E-1)^2] = 1, mean 0: Var(X^2) = 8; independence adds variances. Log-concavity of e^{-t} on [0, ∞) is the definition (log… | CERTIFIED |
| #226 | C_20c | C_20c >= sqrt(3): mu uniform on [-sqrt3, sqrt3] is isotropic log-concave and A = (-inf, 0] has mu(A) = 1/2, mu+(A) = 1/(2 sqrt3) (Patankar) | in Q(sqrt3) through squares: variance 3/3 = 1, (mu+(A)/min(mu(A), 1-mu(A)))^2 = 1/3, so the inverse Cheeger constant of this A is sqrt3 and psi >= sqrt3 | CERTIFIED |
| #226 | C_23b | C_23b <= 1/2: for odd n every off-diagonal entry of G = A^T A is odd, Σ(λ_k − n) = 0 and Σ(λ_k − n)^2 >= n(n−1); Bhatia--Davis gives (λ_max − n)(n − λ_min) >= n − 1, w… | BY READING, not computed — the five sentences of the PR text read against the definition; no number is computed | CERTIFIED |
| #226 | C_16a | C_16a >= 2.156224 from a truncated BDZ2013 extremal on the 2-torus (sums over 0 < |k|^2 <= 4000^2 with c_k = 1/(|k|^2(|k|^2 + 41/5)); δ(u) = S_2/S_1 and the ‖u‖ bounds… | not decided in this campaign — a 50-million-term sum with the PR's own derivation from the BDZ2013 extremal; deciding it needs an interval computation of S_0, S_1, S_2 with a forward error bo… | REFUSED |
| #226 | C_70a | C_70a >= 1.201927 from a cube and a ball in n = 300,000 (Szász's inequality, AM--GM, Steiner's formula, a binomial-κ_{n−j} sum) | not decided in this campaign — a 300,000-term sum of binomial coefficients times volumes of balls with three cited inequalities in the derivation; an interval evaluation with the cited steps … | REFUSED |
| #217 | C_28a | C_28a <= 9: Borsuk's covering assertion fails in dimension 9 — OpenAI's BorsukNine (rank-one projectors onto lines of R^4 under the Frobenius metric; Lean OAI.BorsukNi… | by this repository's own earlier record — nothing new computed: the certificate is the Lean development already decided; the PR's wording ("counterexample to Borsuk's covering assertion", dimension 9) a… | CERTIFIED |
| #210 | Λ (de Bruijn--Newman, registry 21a) | Λ <= 319/2000 = 0.1595 by a "certified record package" (Mosaic Intelligence, 2026-10-03; the registry records 0.2 (PT2021) with Mosaic's own 0.1875* row; the route: co… | the evidence is not in the submission — the package read file by file (nothing run): the scorer (verify/record_score.py, 20 defs) and the two math checkers (math/verify.py with python-flint arb, math/… | REFUSED |
The registry's C₁a is the largest constant with max (f∗f) ≥ C (∫f)² over non-negative f on [−¼, ¼]; any explicit f is an upper bound. Atris's f has 65,536 equal steps with 13-digit rational heights; for a step function the autoconvolution is piecewise linear with its breakpoints on the grid, so its supremum is a grid value — computed here as one exact integer product (the heights packed into a big integer, multiplied, unpacked) and maximised over every shift: 645423412969467179759478160871915520/429496729600000035389440000000000729 = 1.502743486709583379743219592078…, the claimant's own fraction to the last digit, below 1.5027435 by 114163809468…. C₁b likewise: h on 114,688 steps with Σh = n/2 exactly and 0 ≤ h ≤ 1, correlated with 1 − h: 0.380858550316428560109786189090…, below 0.38085856. The registry's entries were 1.502862 and 0.380868.
A single law μ on Z² gives C₃c ≥ H(X−Y)/max(H(X), H(Y), H(X+Y), H(X+2Y)); this certificate mixes two laws across the digits of a base-55 expansion, 39041372760532870645 digits from a 51-point law and 60958627239467129355 from a 47-point law. The entropies add digit by digit only if the map from digit values to L(X,Y) is injective, which holds when every |L(x,y)| on both supports is at most (55−1)/2 = 27 — checked: the maximum is 27. Each per-law entropy is an interval with directed rounding at 128 bits (no code of the claimant's; the single-law instrument that decided C₃b and C₃c in September, with the mixture by rational weights on top); ρ ∈ [1.674894211307116228764343737060, 1.674894211307116228764343737061], above 1.674894211307116. The claimant's flint and PARI checkers print the same 16 digits.
Mosaic Intelligence's submission is 104 files. Its scorer (verify/record_score.py) runs the assembly's verify.py and checks 12 gates — _report_ok, anchor_ok, cover_ok, coverage_ok, criterion_ok, frozen_ok, line_ok, lint_ok, record_lines_ok, rh_ok, script_ok, torus_ok — printing "TOTAL CHECKS RUN: 168846". The two mathematical checkers (python-flint arb; mpmath.iv) evaluate auxiliary quantities on frozen coefficient tables — walls, clocks, norms, debits, Taylor leaves — and compare rationals, hashes and box covers. No function in the 5 scripts evaluates ζ, H_t or the 690,988-term Dirichlet polynomial; the torus floor, the separator at X and the Polymath15 error constants enter as 63 frozen outputs whose proofs cite banks 713, 729, 744, 745, 755, 767, 774, 786, 791 — an internal memory that is not in the bundle. The anchor Λ ≤ 3/16 is the claimant's own 2026-07 row, merged into the registry without review. So the package certifies that its parts fit together as declared; whether the parts are true is not in the submission, and this page refuses rather than guesses. The route itself (collision exclusion with an exterior polydisc floor carried by a "circular heat" lemma) is coherent on reading; the first independent check to run would be the torus-floor inequality on T⁴ by an interval cover, then the separator at x = X for t ∈ [0, 3/16] including y = 0, then the error constants from Polymath15 Theorem 1.3 — each hours to days.