On 2026-10-06 OpenAI published 719 machine-generated manuscripts with Lean formalizations and 416 Comparator challenges. This audit re-ran every check with a second, independent kernel, read every formal statement against the claim it carries, and re-decided every published finite witness in exact arithmetic with code written here. Every proof the kernels finished holds, and every finite object decided here held. The gaps are in what is claimed beyond what is checked — 14 of them, ranked below, each pinned to the file and line of the commit audited.
The release: github.com/openai/math at commit fd4aeeb2 (Apache-2.0; it moved once after our scouting pin adc7f124: 3 manuscripts withdrawn, 14 revised, 11 challenges added). Every gap below was found on 2026-10-10 at fd4aeeb2; when upstream was last checked (2026-10-10 13:25 UTC) its HEAD was still fd4aeeb2, so none of them had been addressed. OpenAI calls the collection partial progress and its formal review "unchecked". Issues and discussions are disabled on the repository. A gap is not an error, a reading is not a certificate, and this page keeps the three apart.
A gap is a place where what is checked is less than what is claimed, where a check the release presents does not do what a reader would assume, or where the means to check a claim are not published. Most of the claims behind these gaps may well be true; a gap says only that the release does not yet show it. Ranked: 1 headline not checked — the headline claim is carried by no machine-checked statement · 2 check weaker than shown — a check the release presents does not check what a reader would assume · 3 cannot be re-checked as shipped — the means to check a claim are not published, or a shipped checker does not check what its paper claims · 4 documentation — the text describing a check is wrong or stale. Each gap names what would close it, and the page refuses to build if a ledger row it rests on changes its word.
Hilbert's sixteenth problem: the uniform bound is in no Lean statement
The family headline leads with the resolution of the uniform boundedness assertion of Hilbert's sixteenth problem: the number of limit cycles of every real planar polynomial vector field is bounded by a constant depending only on its degree. Of the release's 416 statements, only QuinticLienard defines periodic orbits or limit cycles at all, and only for Liénard systems x′ = y − F(x), y′ = −x with deg F ≤ 5 (at most two limit cycles, attained). The linked paper itself calls its problem 'a restricted instance' of Hilbert's sixteenth. The uniform-bound manuscript (September 24) is not linked by the scope note, whose title nevertheless reads 'Hilbert's sixteenth problem: uniform bounds for limit cycles'.
What would close it. State the uniform bound as a Comparator challenge, or say beside the headline that it is not formalized.
Evidence. CONTENTS.md:3443 · 143.md:1-5 · QuinticLienard.lean:40 · introduction.tex:28
Kaplansky: the headline's group is torsion-free; the Lean group is required to have torsion
The family headline is a finitely presented torsion-free group whose group algebra is not directly finite (the October 4 manuscript, over F2). The finitely presented Lean statement REQUIRES the group to contain an element of odd prime order, and lets the field be any finite field of characteristic 2. The linked characteristic-2 paper says so itself: 'The construction uses odd-order torsion and does not assert that K = F2.' The torsion-free manuscript is not linked by the scope note, whose heading is the torsion-free title above a body that describes torsion; the note declares only the nonsofic clause to be outside.
What would close it. Formalize the torsion-free example, or retitle the scope note and the headline to what is formalized.
Evidence. KaplanskyFinitelyPresented.lean:8-10 · 197.md:1-13 · 01-introduction.tex:18 · introduction.tex:14
Penrose inequalities: no Penrose inequality is stated
The family headline claims the sharp enclosing-area spacetime Penrose inequality in every spatial dimension n ≥ 3, with rigidity, charged and higher-dimensional extensions. The family's one challenge, CKSBondiPenrose (3,597 lines), states an area-controlled end replacement and Schwarzschild equality examples; the word 'Penrose' does not occur in it. The scope note links one of the family's 13 manuscripts, and says itself that a conditional inequality kept in the implementation 'is not selected as a substitute for the paper's main inequality'.
What would close it. State the inequality, or present the family as 'supporting results formalized'.
Evidence. CONTENTS.md:6475 · CKSBondiPenrose.lean:3312 · CKSBondiPenrose.lean:3591 · 260.md:5-13
Coarse assembly: the headline is about the maximal map; the Lean is about the reduced one
The headline constructs a space whose MAXIMAL coarse assembly map is not rationally injective (the October 5 manuscript, built on three-dimensional tori). The Lean statement is about the 'ordinary reduced coarse assembly map' (its own docstring), on the September 23 construction from triangular-lattice discs. The October 5 paper says its result 'strengthens the reduced coarse-assembly result' and that the stronger conclusion requires a proof in the universal norm. The scope note links only the September 23 paper, under the maximal title.
What would close it. State the maximal result, or retitle the scope note and the headline.
Evidence. CoarseAssembly.lean:10 · 307.md:1-9 · 01-introduction.tex:46-53
Projected Lax: the formalized cone has an exact lift, by the family's own third manuscript
The headline disproves the Projected Lax conjecture: some hyperbolicity cones admit no finite semidefinite lift, with any number of auxiliary variables (the October 5 manuscript). No challenge states that. HyperbolicCones states that one explicit cone in 23 variables has no semidefinite representation in its original coordinates — and the family's third manuscript gives that very cone an exact semidefinite lift, a pencil of size 100 with 307 auxiliary variables. The formalized cone therefore cannot witness the headline; the cone that does is in no Lean statement.
What would close it. Formalize the cone that has no lift, or say beside the headline which cone the Lean is about.
Evidence. CONTENTS.md:2336 · CONTENTS.md:2354 · HyperbolicCones.lean:68-74 · 095.md:5
Across the release: 34 of 242 formalized families state less than, or other than, what they claim
11 families state a different theorem from their headline, and 23 state less than a manuscript their own scope note links, with nothing saying so. Another 39 headlines lead with results from manuscripts the formalization never linked, so a reader of the headline is not told that no challenge carries them. Every one is listed in §2 with the clause that is missing; each was read twice and is quoted to the line in the statement ledger.
What would close it. One line per family, beside the headline, saying what is and is not formalized.
Evidence. openai-math-statements.json
63 displayed definitions Comparator never compares — one of them carries 'the plane is not 5-colorable'
Comparator compares a declared definition hole by its type only, never its body, and its README says such solutions 'must always be checked with an additional (potentially human) verifier'. 10 configs declare holes; 63 of their 65 holes are displayed with full bodies that a reader takes as the definitions. EuclideanFiveColor's one hole, ProperColoring, carries the whole conclusion; Naimark's seven holes are every predicate of its statement; KServer's nine include MainStatement itself. As configured, the check would accept a solution that redefines any of them with the same type. This audit supplied the verifier the README asks for — a strict run that compares every body constant for constant, and a transfer check in Lean — and settled 9 of the 10 (§3). For DefocusingNLS, whose displayed definition and solution definition differ as kernel terms, neither check settles whether the theorem proves the statement the file displays: that stays open.
What would close it. Take fully written definitions out of definition_names, so Comparator compares them, or ship the extra verifier Comparator asks for.
Evidence. Comparator_Compare.lean:63 · README.md:108-110 · EuclideanFiveColor.json · Naimark.json · KServer.json
Scope notes credit the formalization with theorems no challenge states
Three scope notes say the formalization proves a result whose Lean theorem sits in OpenAI's library but in no challenge, so no reviewed statement fixes what it says and Comparator never compares it: family 132's fixed exponent α > 2 (fixed_power_separation; the config checks only quantitative_separation); family 291's unital Toms–Winter equivalence (unital_main; the config checks only the uniform property Γ theorem); family 210's a = 1 case, vanishing-on-products consequence and reverse equivariant embedding (the config checks only the surjectivity theorem).
What would close it. Add these theorems to the Comparator configs, or stop crediting them to the formalization.
Evidence. 132.md:9 · Separation.lean:36 · SensitivitySeparation.json:4-6 · 291.md:11 · Main.lean:107 · UniformGamma.json:4-6 · 210.md:9 · FoulkesHowe.json:4-6
The independent kernel was switched on for 2 of 416 challenges — and cannot finish the largest as shipped
Comparator can replay every proof through nanoda, a Lean kernel written independently in Rust; the release switched it on for 2 configs (412 false, 2 absent). Here it was on for all: 398 of 416 challenges are accepted by both kernels and none is rejected. But 15 exports overflowed nanoda's hard-coded 16 MiB worker stack — every one of them already accepted by Lean's kernel in the same run. Raising the stack to 1 GiB let 3 of them through; the patch posted in ammkrn/nanoda_lib#44, which makes two of nanoda's definitional-equality checks follow Lean's reference kernel, turned 4 more refused challenges into accepted ones on the stock stack. The others still overflow, and with the patch and a 1 GiB stack they exhaust a 16 GB runner; a 256 GB machine running four of them at once ran out of memory. As shipped, the second kernel cannot check the release's largest proofs on standard hardware.
What would close it. Switch nanoda on for every challenge; upstream, merge the #44 fix and make nanoda's worker stack configurable.
Evidence. lib.rs · openai-math-kernel.yml:86-90 · openai-math-kernel.json
15 headline witnesses are asserted but not published
The counterexamples to Hadwiger's conjecture, the Colin de Verdière chromatic conjecture, Sidorenko's conjecture (its host graph), Ryser's conjecture (two papers) and Kaplansky's conjectures (three papers), and the two cylinder-cover and the bin-packing constructions, are random or 'sufficiently large' constructions given only by a prescription, with no explicit instance; the odd-characteristic Kaplansky example is specified but far too large to check, and the discrete-Fourier word is never printed; the finite non-5-colorable unit-distance graph is obtained by compactness and never displayed; the N(6) = 3 search cites code and data that are absent. Where the Lean is kernel-checked (Hadwiger, Sidorenko, Ryser) the existence is formally proved; the gap is that nobody can look at the object.
What would close it. Publish an explicit instance wherever one can be made, or say in the paper that none is given.
Evidence. openai-math-finite.json
Papers cite checkers and data the release does not ship
N(6) = 3 (mutually unbiased bases in dimension six) cites a verification/code directory of seven programs and an extraction.json — absent, so the computer search behind its headline cannot be re-run. The Thorp-sweep paper cites support/network_bounds.py — absent. The SK-cutoff appendix names numerics-interval.py and numerics-cross-errors.py — absent (the paper calls them non-essential). The cubic three-torus paper says 'the reproducible exact calculations are included with the source' — only the TeX is. The perceptron paper's checker is printed in its appendix, but the reproducibility record it cites is absent. The universal-tensor-squares release records only the exit statuses of the authors' program for 13 ≤ n ≤ 64, with no witness (this audit supplied all 61). The matrix-multiplication 2.258 record library exists only as program state. A valuation relation pins a producer program and an .npz input by hash, neither shipped (its verification does not need them). Each of these was decided here from the text where the text allowed.
What would close it. Ship what the papers cite.
Evidence. execution.tex:16-20 · 04-certificate.tex:294 · scalar-certificate.tex:291-294 · paper.tex:157 · main.tex:9466-9476 · smallcode_verify.py:88-96 · f213_complex_omega.py:85-86 · explicit-relation.json:2-3
Shipped checkers that stop short of what their paper claims — each step re-decided here
Triangular-lattice universal optimality: the shipped checkers 'do not execute the separate floor-rounded matrix construction' the paper relies on (run here, exactly: every table passes). Cycle–clique Ramsey: the 3,099 published deduction traces are 'not offered as proof objects', and no shipped program re-justifies their steps (done here). Campana–Peternell in dimension six: no shipped code forms the 8280 × 6820 matrix or computes its rank 6814 (computed here). Entanglement in dimension ten: no shipped check tests positivity of the state, PPT of the map or trace preservation of the channel (decided here). Einstein zero-plane rigidity: the checker never checks that its triangles tile the domains (checked here). Hadamard matrices of order six: verify.py computes nothing for the cubic-pair obstruction (decided here). Four-state Potts: verify.py hash-binds the two full sign traversals and records 'full_sign_runs_repeated': False. The perceptron: the checker computes none of the analytic constants of the three lemmas, which exist only in prose (checked here). Haldane gap: fixed-width integer arithmetic, with overflow excluded by an a-priori bound and intermediate steps unchecked. One-phase Bernoulli: one shipped check lists the interior expansion as not_verified, and the 'independent' engine that does expand it was written from a specification that already contained the target totals. Mahler: the SymPy check verifies three identities, not the stable rewritings the interval certificate evaluates. Isotropic constants: the checker hand-copies the paper's tables and leaves the non-scalar sections unchecked. Defocusing NLS: the zero counts 2, 1, 0, 0 are derived by hand from a checked sign table (counted here by Routh–Hurwitz). In every case decided here, the mathematics held.
What would close it. Make each checker check the claim, not reproduce the authors' run.
Evidence. README.md:45 · 10-implementation.tex:106-110 · verify.py:128-139 · README.md:38 · f665_einstein_zero_plane.py:60 · f533_hadamard_six.py · verify.py:114 · run_thermal.py:44-48 · algebra-independent.py:205 · tables.tex:931-932 · scalar_identities.py:12-16 · verify_scalar.py:54-66 · exact_verifier.py:145-175
Printed numbers the text alone does not determine
Hadamard matrices of order six: the printed residual of the mixed-moment certificate depends on hand-picked coordinate priority lists that exist only in the authors' program (the paper says the choice 'affects the form of the answer'); re-derived from the text with another priority, the bound still holds, but the printed numbers cannot be reproduced. Triangular-lattice atomic certificate: the pivot claim 0.12 < |pivot| < 1.74 holds only when the twenty unknowns are interleaved (c1, d1, c3, d3, …), an order the paper gives only as 'ordered as c_n, d_n on L' — in block order (all c, then all d) one pivot is 0.103.
What would close it. Print the orderings and priorities the numbers depend on.
Evidence. 05-verification.tex:31-34 · f177_triangular_atomic.py:26-28
Scope notes that are stale or contradict their own challenges
Two scope notes link superseded September editions of manuscripts revised on October 6 (342, Taming implies compatibility; 376, Incompressible box transport); CONTENTS.md lists only the new editions. Family 087's note says the nonsymmetric Mahler conjecture is not included, while its challenge GeneralMahler states it and the same note describes it. Family 129's note puts one-way liveness outside the scope, while OneWayLiveness states it. Family 187's note describes 'four conditional winning templates', while SnakyConditional states an unconditional 35-move win from the empty board. Two support statements import OpenAI's own library, so their definitions come from the claimant.
What would close it. Regenerate the scope notes from the current manuscripts and configs.
Evidence. 342.md:5 · 376.md:8 · 087.md:13 · GeneralMahler.lean:24-31 · 129.md:12 · OneWayLiveness.lean:95-100 · 187.md:11 · SnakyConditional.lean:44-53
OpenAI writes one headline per family; a family can hold several manuscripts and several challenges, and its scope note names the manuscripts the formalization covers. Each family's challenges were read against that headline, clause by clause. The words, least to most severe: MATCHES · NARROWER — DECLARED · NARROWER — UNLINKED · NARROWER — UNDECLARED · DIFFERENT, and SUPPORT-ONLY when every challenge is a declared supporting result. Where two readers disagreed, the less severe word is recorded (40 disagreements, 39 of them only because the first readers did not yet have the UNLINKED word). Every vacuity, junk-value, quantifier and definition flag a first reader marked with a question in the other families was read again: 76 cleared.
| word | families |
|---|---|
| MATCHES | 127 |
| NARROWER — DECLARED | 38 |
| NARROWER — UNLINKED | 39 |
| NARROWER — UNDECLARED | 23 |
| DIFFERENT | 11 |
| SUPPORT-ONLY | 4 |
The 34 DIFFERENT and NARROWER — UNDECLARED families. Each line names what the headline or a linked manuscript claims and no challenge states. Every such row quotes both texts, with file and line, in certs/openai-math-statements.json.
| word | family | claimed, not stated in Lean |
|---|---|---|
| DIFFERENT | 033 · Iitaka subadditivity, variation, and logarithmic additivity | Proves Campana's orbifold Iitaka subadditivity conjecture for smooth Fujiki-class-\mathcal C manifolds with rational simple-normal-crossing boundaries. · For projective fibrations f:U\to V of smooth complex quasi-projective varieties with connected fibers,… |
| DIFFERENT | 058 · Semialgebraic universal covers and bounded domains | Proves the Kollár–Pardon conjecture: the semialgebraic universal covers of connected normal projective complex varieties are exactly products D\times\mathbb C^m\times F, with D bounded symmetric and F simply connected, normal, and projective. · A universal… |
| DIFFERENT | 194 · Lech’s multiplicity conjecture | Proves e(R)\le e(S) for every flat local homomorphism of nonzero Noetherian local rings, where e is Hilbert–Samuel multiplicity. · This resolves Lech's conjecture in every dimension and characteristic. |
| DIFFERENT | 206 · Finite lattice representation and undecidability | Some finite lattices are not congruence lattices of any finite algebra, answering the finite lattice representation problem negatively. · Moreover, no algorithm decides whether a finite lattice has such a representation, or whether it is a full subgroup… |
| DIFFERENT | 218 · Conformal universality for weakly interacting and random-bond Ising… | Weak finite-range square-symmetric even multispin perturbations of the square-lattice Ising model preserve critical bulk spin and energy limits · weak square-symmetric contour interactions also yield chordal SLE3 interface limits. · With sufficiently weak… |
| DIFFERENT | 237 · The three-quarter exponent for honeycomb self-avoiding walk | Proves the diameter form of Nienhuis's predicted three-quarter exponent: a uniformly chosen n-step self-avoiding walk on the honeycomb lattice has diameter n^{3/4+o(1)}. · Its local mass and covering numbers have exponent 4/3. · These estimates hold at every… |
| DIFFERENT | 260 · Spacetime Penrose inequalities: enclosing area, charge, rotation,… | Proves the sharp enclosing-area spacetime Penrose inequality for smooth one-ended asymptotically flat initial data in every spatial dimension n ≥ 3, under dominant energy, weak future trapping, positive enclosing area, and the stated decay assumptions. · It… |
| DIFFERENT | 281 · QAOA attains the SK optimum in the thermodynamic-first limit | Proves that QAOA approaches the ground-state energy of the Gaussian zero-field Sherrington–Kirkpatrick model when system size tends to infinity before circuit depth. · For every accuracy, finite depth and deterministic angles independent of size and disorder… |
| DIFFERENT | 290 · Relative bicentralizers and modular spectral recovery | Proves Connes' bicentralizer conjecture for every type III1 factor with separable predual and every faithful normal state. · More generally, for every inclusion N\subset M of von Neumann algebras with separable preduals admitting a faithful normal… |
| DIFFERENT | 291 · Cuntz comparison, nuclear dimension, and equivariant Jiang–Su… | Proves equivariant Jiang–Su stability for every countable discrete amenable group action on a simple separable unital infinite-dimensional nuclear stably finite Jiang–Su-stable C∗-algebra, resolving this case of Szabó's conjecture without restrictions on… |
| DIFFERENT | 356 · Gigli’s characterization of Alexandrov curvature | Proves Gigli's conjecture: in every integer dimension n ≥ 2, Alexandrov curvature at least κ is characterized by the full-support \mathop{\mathrm{RCD}}\nolimits ((n-1)\kappa,n) condition with reference measure \mathcal H^n and distributional sectional… |
| NARROWER — UNDECLARED | 047 · Zariski cancellation and affine fibrations over the complex numbers | It also disproves the Dolgachev–Weisfeiler affine-fibration conjecture: smooth surjections X\to\mathbb A^1 and \mathbb A^5\to\mathbb A^2 have every residue-field fiber isomorphic to affine three-space but are not Zariski-locally trivial. |
| NARROWER — UNDECLARED | 072 · Brennan's conjecture and the integral-means spectrum | The sharp universal integral-means identity is B_{\mathcal S}(t)=|t|-1 for t ≤ −2. |
| NARROWER — UNDECLARED | 082 · Annular variation and dyadic absolute bounds for the triangular… | Proves maximal and annular r-variation bounds, for every r > 2, from complex L^3(\mathbb R^2)\times L^3(\mathbb R^2) to L^{3/2}(\mathbb R^2). · and gives almost-everywhere and norm convergence |
| NARROWER — UNDECLARED | 089 · Bounded-distortion L1 embeddings of planar and bounded-treewidth… | The corresponding multicommodity flow–cut gaps are uniformly bounded. |
| NARROWER — UNDECLARED | 091 · Logarithmic and Lp Brunn–Minkowski inequalities and the B-conjecture | and the scalar-dilation B-conjecture for all even log-concave Radon measures. · For Lebesgue volume it also proves the additive Lp Brunn–Minkowski inequality for full-dimensional origin-symmetric convex bodies throughout 0\lt p\lt 1. |
| NARROWER — UNDECLARED | 097 · The Euclidean Steinitz–Bergström bound | A matching lower bound gives the optimal order S_2(d)=\Theta(\sqrt d). |
| NARROWER — UNDECLARED | 104 · Quasipolynomial algorithms for mean-payoff, stochastic and parity… | Gives deterministic algorithms using 2^{O((\log(L+2))^2)} bit operations, for complete binary input length L, for ordinary mean-payoff games · and two separate extensions · They compute exact values and optimal positional strategies in ordinary games · the… |
| NARROWER — UNDECLARED | 107 · Matrix multiplication with exponent at most 9/4 | In characteristic zero, some inner dimension na with a > 0.465 permits n^{2+o(1)} rectangular multiplication. · Further square bounds give ω < 2.258 outside finitely many positive characteristics |
| NARROWER — UNDECLARED | 114 · Approximate counting of common integer polymatroid bases | Gives a fully polynomial randomized approximation scheme for counting common integer bases of two integral polymatroids of equal total rank, supplied by exact rank-value oracles. · Capacities are binary-encoded, each integer vector counts once, and oracle… |
| NARROWER — UNDECLARED | 132 · A superquadratic separation of sensitivity and block sensitivity | Constructs total Boolean functions with block sensitivity \mathop{\mathrm{bs}}\nolimits (f)\ge s(f)^\alpha for a fixed α > 2 |
| NARROWER — UNDECLARED | 162 · Counterexamples to Ryser’s covering conjecture | A separate construction over extension fields also disproves Gyárfás's monochromatic tree-cover conjecture. |
| NARROWER — UNDECLARED | 172 · Classification of finite Euclidean Ramsey configurations | It also disproves the Leader–Russell–Walters conjecture that every such configuration is a subset of a finite transitive set. |
| NARROWER — UNDECLARED | 180 · Barnette’s Hamiltonian-cycle conjecture | Equivalently, every three-edge path in a finite simple cubic 3-vertex-connected bipartite Pfaffian graph lies in a Hamiltonian cycle. |
| NARROWER — UNDECLARED | 183 · Power savings for planar halving lines and k-sets | More generally, an n-point set with no three collinear has O(n(k+1)^{1/3-\varepsilon_0}) strictly separable k-subsets for 1\le k\le n/2, with an absolute \varepsilon_0\gt 0. |
| NARROWER — UNDECLARED | 207 · The ℓ¹-Bass conjecture for all discrete groups | Proves the ℓ1-Bass conjecture for every discrete group: Hattori–Stallings traces of idempotent matrices over \ell^1(G) are supported on finitely many finite-order conjugacy classes. · The algebraic companion proves the integral Bass trace conjecture |
| NARROWER — UNDECLARED | 230 · Exact Hausdorff gauges for SLE | Resolves Schramm’s Hausdorff-measure question for chordal SLEκ, 0\lt \kappa\lt 8. · finite measure to every trace segment \gamma([s,t]) · and finite expected measure to the trace in every bounded disk. |
| NARROWER — UNDECLARED | 261 · Localization and delocalization in the Anderson model | Resolves the predicted spectral contrast for the lattice Anderson model with independent uniform site potentials. · In dimension two, every positive disorder strength gives almost surely pure-point spectrum. · In every fixed dimension d ≥ 3, sufficiently… |
| NARROWER — UNDECLARED | 273 · The entropy photon-number inequality | and product thermal inputs attain equality even when their entropies differ. |
| NARROWER — UNDECLARED | 274 · Parity is not in QAC0 | Xu–Li's reductions give the same bounded-error obstruction for strict majority. |
| NARROWER — UNDECLARED | 299 · The Kirchberg–Rørdam character criterion and infinite tensor-power… | Also, the infinite minimal tensor power of every such algebra without characters is Jiang–Su stable, answering the Dadarlat–Toms question. |
| NARROWER — UNDECLARED | 303 · Weak pure infiniteness and Cuntz-algebra absorption | Consequently, every separable nuclear algebra with this property absorbs \mathcal O_\infty, without unitality or simplicity assumptions. |
| NARROWER — UNDECLARED | 326 · The cotype–cotype conjecture under the approximation property | Equivalently, these cotype assumptions force nontrivial Rademacher type. |
| NARROWER — UNDECLARED | 350 · Yau’s nodal bounds: surfaces and higher dimensions | completing Yau's conjecture there · In dimension five, nodal measure can grow faster than \lambda^{1/2+\varepsilon_0} for some fixed \varepsilon_0\gt 0, ruling out even arbitrarily small power losses. |
The 39 NARROWER — UNLINKED families. The headline leads with a result from a manuscript the scope note does not link, so no challenge was ever meant to carry it — but a reader of the headline is not told that.
| family | headline result no challenge states |
|---|---|
| 009 · Function-field reconstruction from Milnor K-theory and Galois data | Reconstructs function fields of transcendence degree at least two over algebraically closed constants from K^{\mathrm M}_1/\ell, K^{\mathrm M}_2/\ell, and their product. · These data recover the perfect closure and constants when ℓ differs from the… |
| 015 · Torus-packet equidistribution in prime, quartic, and sextic degrees | arbitrary-order Picard packets in primitive quartic fields · maximal-order ideal-class packets in primitive sextic fields |
| 039 · Nagata’s conjecture and maximal Seshadri constants | It also proves maximal multipoint Seshadri constants (L^n/r)^{1/n} for every smooth polarized projective variety of dimension n ≥ 2 and all sufficiently large r: at very general points over ℂ · and at the geometric generic tuple over any algebraically closed… |
| 076 · Real ultraflat Littlewood polynomials and unbounded binary merit… | Constructs polynomials with N consecutive coefficients in \{-1,1\} whose modulus is (1+o(1))\sqrt N uniformly on the entire unit circle, for every sufficiently large integer length N. · Thus real Littlewood polynomials are ultraflat, including at the real… |
| 084 · The geometric case of the Erdős similarity conjecture | For every fixed q\in(0,1), constructs compact subsets of [0,1] with measure arbitrarily close to one containing no translated and nontrivially dilated copy of \{q^n:n\ge1\}, with dilations of either sign. · This resolves the geometric-progression case of the… |
| 090 · Triangular-lattice optimality, long-range Riesz and Coulomb… | It also minimizes unit-background renormalized Riesz energies for 0\lt s\lt 2 · and Coulomb energy · resolving Sandier–Serfaty and the two-dimensional Brauchart–Hardin–Saff conjecture on the linear term of optimal spherical logarithmic energy. |
| 095 · Hyperbolicity cones without semidefinite lifts | Disproves the Projected Lax conjecture: some hyperbolicity cones are not spectrahedral shadows. · The examples admit no exact finite affine semidefinite lift, regardless of the number of auxiliary variables or the real coefficients used. |
| 116 · Uniform black-box noncommutative identity testing across… | constructs in deterministic polynomial bit time · For each characteristic |
| 119 · The Courtade–Kumar and Hellinger conjectures | The Hellinger conjecture is also proved for every Boolean output bias and noise correlation. |
| 122 · Quantitative trace-reconstruction bounds with a uniform decoder | A uniform decoder achieves quasipolynomial sample and running-time bounds for known fixed rational retention probabilities. · When the deletion probability is at most n^{-\varepsilon} for fixed ε > 0, both bounds become polynomial in the input and parameter… |
| 143 · Hilbert's sixteenth problem: uniform bounds for limit cycles | Resolves the uniform boundedness assertion in Hilbert's sixteenth problem: the number of isolated periodic orbits of a real planar polynomial vector field is bounded by a finite constant depending only on its degree. |
| 149 · Classwise permanence for weakly reversible mass-action systems | Proves the permanence conjecture for every finite weakly reversible mass-action system with fixed positive rate constants. · Every positive stoichiometric compatibility class, even an unbounded one, has a common compact convex forward-invariant absorbing… |
| 150 · Weak mixing of triangular billiards with an irrational angle | Proves that the billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to π is weakly mixing for normalized area times uniform direction. |
| 175 · Talagrand’s expectation thresholds, discrete convexity, and graph… | An application proves the Ascoli–He–Park–Talagrand graph-decomposition conjecture: every graph's edges split into a universally bounded number of fixed pieces, each with containment threshold at most a universal constant times the original graph's integral… |
| 182 · Power savings for intersective polynomial differences and prime… | For every fixed intersective integer polynomial h of degree k ≥ 2 with positive leading coefficient, proves that a subset of \{1,\ldots,N\} avoiding nonzero values h(1),h(2),\ldots as differences has size O_h(N^{1-c_k}), with c_k\gt 0 depending only on… |
| 184 · Correspondence coloring with a fixed forbidden subgraph | Proves the Alon–Krivelevich–Sudakov coloring conjecture in correspondence-coloring form: graphs avoiding any fixed subgraph F need O_F(\Delta/\log\Delta) colors when their maximum degree Δ is sufficiently large. |
| 186 · Uniform influence and sharp thresholds for graph and hypergraph… | and fixed-uniformity hypergraphs. · and O_r((\log n)^{-r/(r-1)}) for r-uniform hypergraphs, r ≥ 3. · The hypergraph influence bound also applies to nonmonotone properties. |
| 197 · A torsion-free group algebra that is not directly finite | torsion-free · nonsofic · over 𝔽2 · even without torsion |
| 211 · The geometric phase diagram, diffusion, and spectra of random planar… | Critical Fortuin–Kasteleyn planar maps converge to Liouville quantum gravity spheres for 0\lt q\le4 · establishing the surface-to-tree geometric transition. · For FK–Ising and spanning-tree-weighted maps, stationary random walks converge to Liouville… |
| 212 · Planar first-passage geometry and the absence of bigeodesics | Proves that planar first-passage percolation has no doubly infinite geodesic for iid nonnegative nonatomic edge weights when the minimum of four weights has finite second moment. · For exponential weights, the limit shape is strictly convex |
| 215 · Canonical O(3) continuum limit and exact O(4) mass asymptotics | Constructs the canonical continuum limit of the two-dimensional nearest-neighbor O(3) model: a non-Gaussian local relativistic theory with a unique vacuum and a positive mass gap. · For the square-lattice O(4) model, determines the exact leading asymptotic… |
| 220 · Directional zero–one laws beyond iid environments and iid ballisticity | and for stationary ergodic finite-range-dependent environments under uniform ellipticity. |
| 222 · Perceptron free energies and microscopic jamming exponents | Determines finite-temperature variational free energies for Gaussian Ising perceptrons with bounded Borel log-potentials · A spherical extension treats bi-orthogonally invariant disorder with compact limiting singular-value distributions and no outliers. ·… |
| 227 · Critical SK autocorrelation processes and dynamics across the… | For zero-field Gaussian SK heat-bath dynamics with rate-one updates per spin, proves worst-start cutoff on the \log n scale for fixed 0\le\beta\lt 1 · mixing time n^{2/3+o(1)} at β = 1 · and stretched-exponential mixing from a Gibbs-sampled fixed starting… |
| 229 · Exact three- and four-state reconstruction thresholds and four-state… | Proves the exact reconstruction threshold d\lambda^2\gt 1, with nonreconstruction at equality, for three-state symmetric [...] broadcasting on regular trees (d ≥ 2) and observed Poisson trees (mean d > 1 [...] · [...] and four-state ferromagnetic… |
| 247 · An infinite finitely presented residually finite 2-group and a… | Constructs an infinite finitely presented residually finite group whose elements all have finite 2-power order · The construction also yields an infinite-dimensional finitely presented nil associative 𝔽2-algebra and a finitely presented infinite-dimensional… |
| 251 · Amenability, unitarizability, and strong Ulam stability | For countable discrete groups, amenability is also equivalent to strong Ulam stability: sufficiently accurate unitary approximate representations are uniformly close in operator norm to genuine representations on the same, possibly infinite-dimensional,… |
| 256 · Nonsingular systems of equations over arbitrary groups | Proves that every finite system of equations over an arbitrary group whose exponent-sum matrix has full row rank over ℚ has a simultaneous solution in an overgroup, resolving Howie's conjecture. · The coefficient group embeds in the presented quotient. |
| 262 · Sharp finite-matrix Lieb–Thirring inequalities and all equality cases | and arbitrary finite-matrix potentials W ≥ 0 with \int\mathop{\mathrm{tr}}\nolimits (W^{\gamma+1/2})\lt \infty · independent of matrix size. · All equality cases are direct sums, in one constant unitary basis, of scalar sech2 solitons with independent scales… |
| 263 · The ionization and generalized ionization conjectures | For the full nonrelativistic Coulomb model with two electron spin states, proves that a molecule with M fixed nuclei of charges at least one and total charge Z strictly binds at most Z+CM electrons. · Neutral-atom first ionization energies and radii… |
| 267 · Positive-temperature Bose–Einstein condensation and exact quantum… | Proves Bose–Einstein condensation for the exact canonical Gibbs state of the three-dimensional hard-sphere gas: each fixed exclusion distance and sufficiently small fixed density admit a strictly positive temperature, independent of volume, with positive… |
| 271 · Bloch's law, its lattice correction, and the spherical magnetization… | Proves Bloch's T3/2 law with its exact coefficient for three-dimensional quantum Heisenberg ferromagnets at every positive quantum spin, allowing nonnegative symmetric finite-range couplings whose support generates ℤ3. · The thermodynamic limit precedes the… |
| 289 · Strong Kadison–Kastler stability and its spatial boundaries | Counterexamples show that near-identity conjugacy fails for one-sided near inclusions · and that arbitrarily close norm-separable C∗-algebras need not be ambiently unitarily conjugate. |
| 307 · Failure of rational injectivity for maximal coarse assembly | Constructs a uniformly discrete bounded-geometry space whose maximal coarse assembly map is not rationally injective. · The example is a coarse disjoint union of finite connected graphs of uniformly bounded degree, with an infinite-order kernel class. |
| 337 · Sharp Cartan–Hadamard isoperimetry and rigidity | Proves generalized Cartan–Hadamard isoperimetry in every dimension: in a complete simply connected manifold with sectional curvature at most κ ≤ 0, every finite-volume finite-perimeter set satisfies the sharp comparison with the equal-volume model ball. ·… |
| 348 · Nonnegative-curvature Einstein classification and an L2 topological… | Classifies closed connected Einstein four-manifolds with positive Einstein constant and nonnegative sectional curvature: up to scaling, their universal Riemannian covers are the round S4, Fubini–Study \mathbb{CP}^2, or a product of equal round two-spheres. ·… |
| 353 · Affine Bernstein rigidity through dimension nine and a smooth… | A smooth entire nonquadratic example in dimension ten makes this range sharp. · In dimensions three through nine, the paraboloid classification also holds for connected open locally uniformly convex affine-maximal hypersurfaces complete for the affine… |
| 361 · Failure of integer-degree harmonic dimension comparison | For every sufficiently large integer k, a complete smooth metric on ℝ3 has at least (k+2)^2 independent harmonic functions of growth at most k, exceeding the Euclidean count (k+1)^2. · The metric may depend on k. |
| 365 · Joint metric and connection recovery from one boundary patch | Zero-frequency measurements on any nonempty open boundary patch determine a smooth metric and smooth unitary connection on a trivial Hermitian rank-two bundle over a compact connected manifold of dimension at least three, up to diffeomorphism and gauge fixed… |
10 challenges list definitions in definition_names. For those, Comparator compares the definition's name, universe levels, type and safety — never its body (Comparator/Compare.lean, definitionHoleMatches, at the pinned revision) — and its own README says such solutions "must always be checked with an additional (potentially human) verifier". Of the 65 holes these files declare, 63 are displayed with a full body and 2 are left sorried: a reader of the challenge sees 63 definitions the check does not compare. Lane K supplies the missing verifier twice over: a strict run with the holes emptied, which compares every body constant by constant, and a transfer check in Lean.
| challenge | holes (displayed) | bodies, decided | transfer | displayed statement |
|---|---|---|---|---|
| Brenier | 12 (12) | SAME BODIES | TRANSFERS | PROVED |
| DefocusingNLS | 3 (2) | BODIES DIFFER OAI.DefocusingNLS.sobolevOddPower | NOT DEFINITIONAL | OPEN |
| ElementaryPositivity | 1 (0) | SAME BODIES | NOT DECIDED | PROVED |
| EuclideanFiveColor | 1 (1) | SAME BODIES | TRANSFERS | PROVED |
| KServer | 9 (9) | SAME BODIES | NOT DEFINITIONAL | PROVED |
| LogspaceEquality | 20 (20) | SAME BODIES | NOT DECIDED | PROVED |
| Naimark | 7 (7) | SAME BODIES | TRANSFERS | PROVED |
| OccupiedOverlap | 5 (5) | BODIES DIFFER OAI.RowColumn.OccupiedOverlapEndpoint | TRANSFERS | PROVED |
| Rokhlin | 4 (4) | SAME BODIES | TRANSFERS | PROVED |
| SpinAngle | 3 (3) | BODIES DIFFER OAI.SpinAngle.missingInRow | TRANSFERS | PROVED |
The transfer column (pre-registration amendment 9) asks Lean itself whether each theorem proves the statement the file displays. The challenge file's skeleton is kept; its holes, and every declaration tied to them, are copied under new names; every other name resolves to the solution's constant, which Comparator has already matched to the challenge's. A guard computed in Lean refuses the check if a copy reaches an original hole or a constant Comparator never compared, and each solution theorem is then offered as a proof of the copied statement. TRANSFERS needs Lean's kernel to accept it AND a red control — one displayed body forged — to be rejected. A NOT DEFINITIONAL or a guard refusal can be the method's limit rather than a difference, so the last column counts a statement as proved when the strict run found the same bodies OR the transfer holds, and leaves it open otherwise.
Where the strict run names a constant whose bodies differ (OAI.DefocusingNLS.sobolevOddPower, OAI.RowColumn.OccupiedOverlapEndpoint, OAI.SpinAngle.missingInRow), the source text reads the same in the challenge and the solution; the kernel terms differ through elaboration. DefocusingNLS: the transfer check did not settle it (NOT DEFINITIONAL); OccupiedOverlap: the transfer check settles it — the theorem proves the displayed statement; SpinAngle: the transfer check settles it — the theorem proves the displayed statement.
Comparator builds a challenge and its solution in a sandbox, exports both, checks that each listed theorem has exactly the challenge's statement and uses no axiom beyond propext, Quot.sound and Classical.choice, and replays the proof through Lean's kernel and any external kernel it is given. The release enabled nanoda for 2 challenges; here it is on for all. One job per challenge, on GitHub's Linux runners (4 vCPU, 16 GB; the sandbox is Linux-only). A CERTIFIED here says the Lean theorem is proved; whether that theorem is the paper's claim is §2.
398 of 416 CERTIFIED, none rejected. The 18 REFUSED are 2 nanoda stack overflows (16 MiB thread stack), 13 jobs the runner terminated in Comparator (1 GiB stack, 16 GB machine), 3 jobs that hit the runner's time limit. Every one of the 15 exports that overflowed nanoda's stack had already been accepted by Lean's kernel in the same run (15 of 15); with the stack raised to 1 GiB (pre-registration amendment 11), 3 were then accepted by nanoda as well. The 18 challenges the hosted runners could not finish were sent to one 256 GB RunPod machine four at a time (pre-registration amendment 14); it ran out of memory, no result was recovered, and the operator chose not to retry — they stay REFUSED, for resources, never counted against the release. The overflows and the memory exhaustion are the two symptoms traced in ammkrn/nanoda_lib#44 (open since 2026-10-06, with a patch that makes nanoda's definitional-equality checks follow Lean's reference kernel); re-run with that patch (pre-registration amendment 13), 4 of the 22 refused challenges are accepted by both kernels, 4 of them on nanoda's stock 16 MiB stack; every row accepted that way says so in the ledger.
| verdict | challenge | family | why |
|---|---|---|---|
| REFUSED | BinPackingGap | 118 | fatal runtime error: stack overflow, aborting | uncaught exception: nanoda exited with 134 | Command exited with non-zero status 1 |
| REFUSED | Catalan | 005 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | CoarseAssembly | 307 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | ContinuumCoulombHardness | 275 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | CycleCliqueRamsey | 189 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | DirectedFeedback | 102 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: The hosted runner lost communication with the server.… |
| REFUSED | ErdosReciprocal | 159 | the job stopped before Comparator ran (see the run log) |
| REFUSED | IndependentSets | 106 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | MinUncut | 102 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | MUBSix | 266 | the job stopped before Comparator ran (see the run log) |
| REFUSED | NuclearUltrapower | 292 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | OptimalMaxCut | 102 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | PerfectCompleteness | 105 | fatal runtime error: stack overflow, aborting | uncaught exception: nanoda exited with 134 | Command exited with non-zero status 1 |
| REFUSED | PlanarPacking | 090 | the job stopped before Comparator ran (see the run log) |
| REFUSED | SquareDifference | 182 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | UniqueGamesTheorem | 102 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | UniversalTensorSquares | 205 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
| REFUSED | VertexCover | 102 | the job ended (failure) in the step "comparator, Lean's kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.) |
CERTIFIED, each by Lean's kernel and nanoda: AbhyankarSathaye AffineBernstein AlgorithmicThinTrees AmplitudeDamping ArnoldCounterexample ArtinCAT0 ArtinParabolicIntersections AsymptoticallyMinimalLittlewood AtomicGaussian AuslanderReiten BackwardIntertwiners BalancedBoxRouting BalancedRyser BalancedThreeStack BallPacking BallPackingNecessity BarnetteHamiltonian BassTorsionFree BassTrace BenjaminiSchramm BernoulliNonflatInSeven BiholderTransport BinaryEditLower BinaryMatching BinarySweep BipartiteCrossing BogomolovPopInjectivity BoltzmannNonuniqueness BooneHigman BorsukNine BoundedRecovery BoundedTreePotentials BoundedTreewidthL1 Brenier Brennan BrennanSharp BufferedIsing C0Absorption C1EntropyCounterexample CannonGeometricAction CartierChartCompactnessSupport CayleyPercolation CharacterCriterion CharacterVarietiesAllSeamsSupport CHObstruction ChoicelessPolynomialTime CirculantHadamard CKSBondiPenrose ClassicalON CliqueFreeLog CoboundaryExpanders CommonBasesFPRAS CommutingDerivations CompactBanach CompleteCrossing CompleteCrouzeix ComplexCancellation Conductivity ConjugatePoints ContingencyTables ContinuousCircleWeight ContinuumTransition CoordinateSweeps CoordinateTrace Cotype CoulombCounterexample CoulombIonization CoulombRadii CourtadeKumar CoveringDensity CriticalPercolation CriticalSK CriticalSKMixing CriticalStripMass CriticalZ3 CrouzeixHilbert CubicTorus CycleDecomposition CylinderCovering DaugavetModuli DefocusingNLS DegreeRigidity DeligneDrinfeld DepthFive DepthThree DiamondDistortion DilutedSpin DimensionTenChannel DimensionTenPair DirectCrouzeix DirectionalBallisticity DirectionalWalk DirichletSevenEighths DiscreteLipschitzFree DiskMaximal Dixmier DixmierAllDiscrete DoublingHilbert DukePrimeDegree DuttaDomain DyadicAvoidance EditApproximation EditDistance EgyptianFractions EilenbergGanea EinsteinFour ElasticityUniqueness ElementaryPositivity EntangledGames EntropyPhotonNumber EuclideanFiveColor EuclideanRamsey EuclideanRamseyCircle EuclideanRamseyNine EuclideanRamseyQuadratic EuclideanRamseySpherical EuclideanRamseyTransitive EvenBarker ExactFourier ExactInfiniteness ExactQuantumFactoring FactorGeneration FalconerAllDimensions FillingCoefficient FiniteCircle FiniteCongruenceGraph FiniteEntropySeparation FiniteFactor FinitisticAsymmetry FixedClauseThreshold FKCRT ForcedNavierStokesComputation ForestSpace FormulaHitting FoulkesHowe FourierLLogL FourRowPermanent FreeIsing FreeUniformSpanningForest GammaPassage GaussianFiniteEntropy GaussianInformation GaussianMoat GaussianPropeller GaussianReplacement GeneralizedStarHeight GeneralMahler GotsmanLinial GrahamSpherical GrothendieckElementaryExpansion GroupRingDeterminant HadamardCubeFiber HadwigerCounterexample HalvingLines HardSphere HarmonicArtin HarmonicGrowth HeckeSevenEighths HeilbronnTriangle Heisenberg HenonEmden HilbertCrouzeix HoneycombBridgeFiniteness HoneycombBridgeMassSupport HoneycombFreeEnergy HotSpots HyperbolicCones HyperbolicObstruction HyperinvariantSubspaces IndependentProducts IndividualStrongInfiniteness InfiniteMatroid InfiniteMatroidCorollaries InterpolatedFactors InvariantIsing IrrationalRotation IrrationalTriangleBilliard IsingFiniteness IsometricImmersion Jacobsthal JacobsthalImproved JointDickman KadisonRingrose KadisonSimilarity KahlerSplitting KaplanskyDirectFiniteness KaplanskyFinitelyPresented KaplanskyQuasitrace KaplanskyStableFiniteness Kervaire KLInvariance KMedianRecovery KMedianRefinedRecovery KMedianThreshold KoebeCircleDomains KServer Laughlin LaughlinFock LaughlinGap LaughlinPlanar LiebThirring LipschitzEquivalence LipschitzHilbert ListHadwiger LittleFinitistic LittlewoodFiniteFlatness LogBrunnMinkowski LogConcaveQuery LogKodairaFiberNegative LogspaceEquality MahlerConjecture MarkovType MassAction MatchingAffineLift MatchingEntropy MatchingEntropyBounds MatchingFPRAS MatchingPSD MatrixFields MatrixMultiplication MatrixRemoval MatroidProphet MatroidSecretary MaximalSeshadriConstants MemoryPrecision MetricEntropyDuality MetricKMedian MidpointLenses Nagata Naimark NavierStokesAlternating NavierStokesVelocity NodalLength NoiselessRegression OccupiedOverlap OddKaplansky OneTapeSpace OneWayLiveness OrdinaryElliott OrdinaryTwoPointCorrelations OstmannComplete OstmannPrimes ParityLifts PartialPermutation PartitionConsistency PartitionPrinciple PattersonFirstMoment PerceptronFreeEnergy PeriodicGroup PeriodicTilingThree PermanentCubic PettyProjectionVolume PiExponent PinchedKahler PinnedDistances PlanarAndersonSpectrum PlanarFalconer PlanarFirstPassage PlanarL1 PlanarUnitDistances PlaneColoring PolycyclicRecognition PosteriorReplicas PowerFreeValues PrimeGaps ProductBrown ProjectionCounterexample ProjectionMoments ProjectionVolume QACParity QuadricBundles QuantitativeVanDerWaerden QuasiRiemannHypothesis QuinticLienard RadialDensityInterval RadialTransition RamseyFive RandomizedMeanPayoff RationalHitting RealL1Renorming RecursivePotentials ReflexiveFixedPoints RegularParity RelativeGeneration RieszQuantitative Rokhlin RuledCovering RyserCovering RyserOddExtensions SATComputability SATSharpness SATVariance Saxl SecondKahnKalai SelfSimilar SelfSimilarCorollaries SensitivitySeparation SeparableQuotientNegative SeymourSecondNeighborhood SharpCAT0Filling SharpLogRamsey SharpThreshold ShortEgyptianFractions SidorenkoCounterexample SiegelZeros SignedFiniteBand SignedSweepMoment SimpleAmenable SimpleOvergroups SingleFold SingleLatticeCovering SingletonLoopMatching SKBarriers SKFullSupport SKHighTemperature SKRatio SKValue SLELowerPositivity SmoothInitialForm SmoothObstruction SmoothYau SnakyCertificate SnakyConditional SnakyTwentyOne SoftChannel204 SolenoidalSheetPrograms SphericalField SpinAngle SplitTangentIntegrability SquareRootDegree StableCoordinateFour StandardMapComponents StandardMapEntropy StandardMapLyapunov SteinitzBergstrom StrictMeans StrongKadisonKastler StronglyRayleighDPP StrongThinTree StructuralCrouzeix SubpolynomialLp SubsphereCurrent Superstring SurfaceConeCandidateSupport SurfaceImmersion SwitchChain SymmetricDomains SymmetricMahlerEquality SymmetricPolar Tachikawa TalagrandDiscreteConvexity TalagrandExpectationThreshold TamingCompatibility ThomasonModelStructures ThompsonNonamenability ThorpFirstReciprocal ThorpRemaining ThorpRouting ThorpWeightedCompatibility ThreeMachine ThreeStateSupercritical ThreeStateTreeClauses ThreeTorus TingleySphereIsometry TorsionFreeHyperbolic TorsionFreeZeroDivisors TotientAsymptotic TotientCompanionZero TraceIdealTransportSupport TraceReconstruction TreeEdit TriangleFace TriangleRemoval TriangularCovering TriangularEnergy TriangularGaussian TriangularHilbert TruffetCounterexample TwoWayComplementation TwoWayDeterminization TypeSystemNormalization UniformCommutator UniformFourier UniformGamma UniformKServer UniformSparsestCut UniversalFInfinity VariableWL VelocityHemisphere VertexAlgebraNet VlasovMaxwell WeakHessian WeakMTWGlobalSupport WeightedSweepMoments WeisfeilerLeman WitnessedChoice WLIdentification YauCounterexample.
The trust base, as the pre-registration states it: the two kernels, lean4export, Comparator's comparison code, landrun's Landlock sandbox on the runner (recorded per job; Comparator calls landrun with --best-effort, so the job records the kernel's LSM list), the Mathlib cache fetched by lake exe cache get, and GitHub's runners. Comparator's README also asks for systemd-run with AF_UNIX restricted; GitHub's runners have no user systemd session, so that guard is NOT applied, and the page says so.
A census of all 719 abstracts, by three readers on disjoint slices, named 66 finite cores over 65 manuscripts before any was decided: 47 published and checkable, 4 published but expensive, 15 asserted but not published in checkable form. Each decider reads the release's own bytes and records their sha256; "whole headline" means the finite object is the entire claim, otherwise the analytic argument around the component is not decided here. 44 CERTIFIED (3 of them the whole headline: An explicit noncoordinate polynomial with affine three-space zero fibre; A product counterexample to the simplex maximum for projection-body volume; Snaky in 21 Maker moves), 0 REFUTED, 7 REFUSED (decided in part, or too costly here, each cost named), 15 NEEDS DATA.
| verdict | row | manuscript | what is decided |
|---|---|---|---|
| CERTIFIED | F-009 | Catalan's constant is irrational | a finite component: the three finite components of the proof and their comparison, not the headline. (1) the real-place certificate — for the published trial sequences, the right side of eq:energy-dual is <= -2.290939875 (kappa=2) and… |
| CERTIFIED | F-045 | Squarefree values of quartics and power-free values of polynomials | a finite component: the exact parameter certificate of Proposition prop:parameter-certificate (all 3,989 cells for d = 4..8, Table tab:parameter-certificate, the 150 endpoint derivative inequalities), the printed exponent margins, and the… |
| CERTIFIED | F-103 | An explicit failure of complex affine-space cancellation | a finite component: the cylinder isomorphism A[w] = C^[5] (Proposition prop:stabilization), by the paper's printed maps with inverses; NOT A not = C^[4], which carries the counterexample |
| CERTIFIED | F-105 | A stable coordinate that is not a coordinate in four variables | a finite component: f is a one-stable coordinate (an explicit automorphism of C[x1..x4,w] with exhibited inverse sends f to x1), deg f = 5, and every fibre f = lambda is C^[3]; NOT that f is not a coordinate in four variables, which… |
| CERTIFIED | F-106 | An explicit noncoordinate polynomial with affine three-space zero fibre | the whole headline: R/(F) = C^[3] by the paper's printed mutually inverse maps, and grad F vanishes at a point, so F is not a coordinate |
| CERTIFIED | F-125 | Ambiently homeomorphic isolated hypersurfaces of multiplicities two and three | a finite component: Lemma seed:product (the integer relation with E > 0 and both products 1), by the shipped witness and by the printed F_1009 rank certificate, plus the chain arithmetic; not the spectra, the lattice/topology, or the… |
| CERTIFIED | F-135 | The Campana–Peternell conjecture in dimension six | a finite component: Lemma lem:finite-ratio (from the matrices A, C_1, N defined in Section 4, N(xi_i eta_j) = 0 with xi_0 = eta_0 = 1 forces 32 - 20 eta_1 + 3 eta_1^2 = 0); dim_Q K_3 <= 6 by a rank mod 10007 (a certified lower bound on… |
| CERTIFIED | F-171 | The Mahler Conjecture for General Convex Bodies | a finite component: the finite certificates of Appendices 07-08 (the 152-node profile enclosures and every printed node bound and finite sum; the stable-formula identities; the layer rectangles; the chord-error, tail-vector, interpolation… |
| CERTIFIED | F-174 | A product counterexample to the simplex maximum for projection-body volume | the whole headline: K = T10 x T10 violates the proposed simplex bound in dimension 20, with the exact ratio printed |
| CERTIFIED | F-177 | An atomic certificate for triangular-lattice universal optimality | a finite component: every inequality of Lemma lem:finite-certificate (the two 20x20 interval blocks and their inverses, the parameter polytope, the jet / curvature / Taylor envelopes, all 659 Bernstein row minima) and the printed rational… |
| CERTIFIED | F-178 | Universal optimality of the triangular lattice | a finite component: Proposition prop:finite-certificate through its three stronger tables (27 power, 30 column, 37310 Bernstein and 10 tail comparisons) on enclosures of the exact quadrature arrays, the same tables on an exact execution… |
| CERTIFIED | F-179 | A sharp Fourier certificate for planar circle packing | a finite component: every finite certificate the proof cites -- Lemma interpolation:finite (the two inverse certificates via W_+-, the exterior block, the 204 residuals, the table norms) and Lemma signs:bernstein (2436 Bernstein… |
| CERTIFIED | F-180 | Triangular minimality for planar Coulomb renormalized energy | a finite component -- the whole finite certificate of Section sec:computation (Proposition comp:finite-soundness), by an independent route: the 38 lattice coefficients (two ways) and |c_1| < 1; lambda, mu, K, B(l), f_0(l), f(l), -pi B(l)… |
| CERTIFIED | F-189 | The Gaussian propeller bound in every dimension | a finite component: every finite numerical comparison and enclosure of the m >= 5 exclusion (Appendix cert:arithmetic, Tables sc:interval-table, cert:quantiles, elim:small-table, elim:four-table, elim:final-table and the inline bounds),… |
| REFUSED | F-195 | Finite angular cylinder covers below the half-area bound | a finite component: A_min(K) = sqrt 2, the construction's parameters, every polynomial identity of the coverage proof, and the exact total base area at eps = 1/2000 and tau = 1/4000 (strictly below A_min/2, inside the printed remainder… |
| NEEDS DATA | F-197 | Slope-field perturbations of the two-cylinder covering | NOT PUBLISHED as a specific instance; construction in preprints/Slope-field-perturbations-of-the-two-cylinder-covering-September-27-2026/build/sections/threshold.tex and dictionary.tex with non-explicit smallness thresholds. |
| NEEDS DATA | F-198 | Finite triangular approximation of radial sweeps | NOT PUBLISHED as a specific instance; preprints/Finite-triangular-approximation-of-radial-sweeps-September-27-2026/build/beams.tex l.292 ('For every zeta > 0, the tetrahedron K has a finite cylinder cover ...'), coordinates.tex. |
| CERTIFIED | F-199 | A sharp entropy bound and the simplex inequality for isotropic constants | a finite component: the scalar certificate behind Lemmas sc:bounds and tr:scalar-basic — the central piecewise-polynomial certificate on [-6,10] rebuilt from its eleven seed pairs (residuals, joins, anchors, error budgets, all 44 group… |
| CERTIFIED | F-209 | Randomized quasipolynomial-time mean-payoff games | a finite component (the appendix side result, not the main theorem): on the printed two-variable instance the true minimum is exactly 0, while the substitution rule as formalised in the challenge is forced through x2 = h, x1 = h + 1 to… |
| REFUSED | F-213 | Complex Matrix Multiplication Below 2.258 and Rectangular Bounds | finite components only: the three rectangular witnesses (alpha > 0.465, w(0.709) < 2.092, family omega < 2.267) as finite computations; for omega < 2.258 the barrier, both charts (the 18 MB chart verified as the recursion's output), the… |
| CERTIFIED | F-214 | Staggered extraction for exact matrix multiplication over every field | a finite component: the parameter certificate — the five integer arrays, decoded by the printed rules and contracted by the printed finite formulas, give every printed table value and enclosure and 3(8 log 7 - H_0 - C_*)/S_* <… |
| NEEDS DATA | F-232 | Additive hardness and unbounded configuration gaps in bin packing | preprints/Additive-hardness-and-unbounded-configuration-gaps-in-bin-packing-September-24-2026/build/source/consequences.tex l.9-24 (proof of Theorem thm:unbounded-gap), /build/source/instance.tex l.26-60 (parameters eq:parameters and… |
| CERTIFIED | F-234 | Hellinger contraction with arbitrary Boolean output bias | a finite component: the scalar certificates of the proof — the induction parameters, the 17 profiles' five Bernstein sign checks, the three-coordinate base table, the 21-box pair interval certificate, and every finite comparison and… |
| NEEDS DATA | F-248 | An explicit power saving for the exact discrete Fourier transform | Interface and lemma in build/sections/synthesis.tex lines 18-60 (Lemma syn:local-certificate at lines 39-46), built from the network of build/sections/network.tex (matrix eq. net:C at line 6; Prop. net:finite-interface at line 370;… |
| CERTIFIED | F-262 | Subset Sum in Time O(2^{0.49n}) | a finite component: the numerical certificate of Proposition prop:filtering-moments (Appendix app:numerical) - every printed enclosure, error bound and comparison recomputed in directed rational interval arithmetic; the analytic trapezoid… |
| CERTIFIED | F-287 | Arithmetic classification and non-Pisot singularity for Bernoulli convolutions | a finite component: the root location of the degree-31 polynomial (all 31 roots isolated, beta in (1.8392, 1.8393) the only real root, alpha the only other expanding pair, beta not Pisot) and every printed integer of the rational moment… |
| NEEDS DATA | F-294 | A counterexample to Hadwiger's conjecture | NOT PUBLISHED. Theorem thm:main in build/sections/01-introduction.tex lines 20-27; sampling of raw vertices in build/sections/02-geometry.tex lines 258-320; parameter order in build/sections/14-parameters.tex. |
| NEEDS DATA | F-295 | A counterexample to the Colin de Verdière chromatic conjecture | NOT PUBLISHED. Theorem thm:main at build/sections/01-introduction.tex line 42; base graphs Theorem thm:base-graphs at line 147; 'm=2^{1000gN} is the sampled graph order' at lines 315-317. |
| CERTIFIED | F-297a | The Euclidean plane is not five-colorable | a finite component: Lemma angular-certificate (all seven placed Moser-spindle vertices strictly in the region 0<l<4, P<P'), the eleven unit edges and non-3-colourability, and every number of the paper's rational verification. NOT the… |
| NEEDS DATA | F-297b | The Euclidean plane is not five-colorable | NOT PUBLISHED. build/sections/introduction.tex lines 31-36 ('an unrestricted lower bound can also be established without first displaying a finite graph witnessing it') and lines 309-313 ('Theorem~\ref{thm:main} and graph compactness ...… |
| NEEDS DATA | F-300 | A counterexample to Sidorenko's conjecture | H: build/sections/complex.tex Table tab:complex at lines 19-56 (Theorem thm:main in build/sections/introduction.tex lines 18-26; Lean ComparatorChallenges/SidorenkoCounterexample.lean def faces). Host: NOT PUBLISHED.… |
| NEEDS DATA | F-301 | Balanced counterexamples to Ryser's conjecture at prime orders | NOT PUBLISHED. Random choices in build/candidates.tex lines 75-140; the random selection procedure in build/selection.tex lines 20-35 ('All subsequent assertions concern sufficiently large q', line 93). |
| NEEDS DATA | F-302 | A counterexample to Ryser's covering conjecture | NOT PUBLISHED. build/selection.tex lines 1-60 (independent random shifts; Lemma sel-domination at line 52). |
| CERTIFIED | F-336 | Snaky in 21 Maker moves | the whole headline (Theorem thm:main, 21 Maker moves on Z^2) and Corollary cor:finite-board, twice: (I) the certificate evaluates to A_727 = {}, h_727 = 21 under the paper's combination rule — sound only with Lemma lem:combination, proved… |
| CERTIFIED | F-338 | Cycle--clique Ramsey numbers | a finite component: the 3099 published deduction traces of Proposition finite:verified exclude all 3099 (pattern, k, t) instances by the paper's stated rules, applied correctly (the rules' soundness and the reduction of R(C_m,K_n) to… |
| CERTIFIED | F-339 | Polynomial removal fails for ordered binary matrices | a finite component: Theorem thm:main at h = 1 and h = 2 (A_1 776 x 776, A_2 3,096 x 3,096), both inequalities decided exactly (N_H(A_h) = 2 m^130 by an exhaustive ordered-copy search; dist_H(A_h) >= eps_h by the sampling argument with… |
| NEEDS DATA | F-345 | A Torsion-Free Group Algebra with Zero Divisors | NOT PUBLISHED. build/sections/factors.tex lines 31-35: 'The construction is probabilistic: it proves that suitable finite matchings exist, without specifying matchings from which a concrete presentation and zero-divisor factors can be… |
| NEEDS DATA | F-346 | A Torsion-Free Group Algebra That Is Not Directly Finite | NOT PUBLISHED; the construction is probabilistic. Section sections/random.tex (input at build/paper.tex line 44); build/sections/topology.tex line 3 ('The probabilistic argument has produced finite immersed graphs');… |
| NEEDS DATA | F-347 | A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic… | Not in checkable form. build/sections/01-introduction.tex lines 8-15 (theorem and 'terminating prescription'); build/sections/04-hypergraph.tex lines 8-20 and 53 (parameters, random slabs, 'for all sufficiently large h'). |
| NEEDS DATA | F-349 | A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd… | Specified but infeasible. Theorem op:main in build/sections/01-introduction.tex lines 14-30; finite data in build/sections/02-finite-data.tex; explicit idempotent eq op:explicit-e in build/sections/03-modular.tex line 191. |
| CERTIFIED | F-351 | An explicit counterexample to the Auslander-Reiten conjecture | a finite component: the ten-dimensional algebra C, its trivial extension T and trace, the 179-entry cochain (cocycle and boundary identities, evaluation q^3), the resolution of s over C for every i, and the finite identities of the lift —… |
| CERTIFIED | F-352 | A counterexample to Tachikawa's second conjecture | a finite component: the ten-dimensional algebra C (and its identity with the companion paper's), T and its symmetrizing form, E = T (x) T symmetric nondegenerate, the corner table of B, the exact sequences of Prop a:dual-dimensions, the… |
| CERTIFIED | F-360 | Universal Tensor Squares for Symmetric Groups | a finite component: Proposition prop:finite-check for every eligible n <= 64 (61 of the 61 degrees), with witnesses supplied and certified here (the release records none: NEEDS DATA for its own certificate); the large-degree theory (n >… |
| REFUSED | F-369 | Foulkes' conjecture for the sixth symmetric power | decided in part (pre-registration amendment 5): the base range is decided for b = 6..12 in the ledger run (b = 6..15 in a separate run of this session); b = 13..25 (estimated 8-12 CPU-hours) and the partitions outside the band at b =… |
| REFUSED | F-409 | Microscopic jamming in the negative spherical perceptron | a finite component: stage (I) of the certificate — the two final spectral tests (.2936535023 < lambda(.2936533) < .2936535043, .2936533037 < lambda(.2936535) < .2936533057, hence lambda(a) - a changes sign on (.2936533, .2936535)) by own… |
| CERTIFIED | F-426 | Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase | a finite component: Lemma rcut:lem:scalar-data and Table rcut:tab:scalar-intervals of the appendix route (the independent beta < 1/2 proof) - the 205 quadrature terms, every finite enclosure, the whole error budget and every interval… |
| REFUSED | F-433 | The Reconstruction Threshold for the Ferromagnetic Four-State Potts Model | decided in part (pre-registration amendment 5): the product inequality (b) is decided only on C x S, S x C and C' x C' (about 0.4% of S x S by volume; the rest projected above 20 CPU-hours at ~5 s per cell); the scalar certificate and… |
| REFUSED | F-435 | The exact reconstruction threshold for the three-state symmetric channel | decided in part (pre-registration amendment 5): the interval certificate is decided only for q <= 4/5; q > 4/5, which holds the near-uniform corner where P ~ 2e-5, is not (extending band 2 to q <= 9/10 alone took 84,610 boxes and 1,916… |
| CERTIFIED | F-467 | Routing densities and representation contraction for Thorp sweeps | a finite component: the five rational inequalities of Section 4 (H(1/8), H(13/50), H(1) and the two entropy brackets at 7/25 and 1) with every supporting finite fact the text states (closed form of h_j from its definition, h_j <=… |
| NEEDS DATA | F-532 | The maximum number of mutually unbiased bases in dimension six | Algorithm and error analysis in build/sections/{seed,completion,phase-cover,refinement,exclusion,rounding,execution}.tex (5,886 tex lines). The code and data are NOT PUBLISHED in the clone: build/sections/execution.tex:16-20 names… |
| CERTIFIED | F-533 | Exact Fourier certificates for complex Hadamard matrices of order six | a finite component: the exact finite core of both theorems — the single-matrix certificate (Prop. pair-certificate, both q), the finite arithmetic of the cubic-pair obstruction (Prop. cubic-exclusion), and the mixed-moment certificate… |
| CERTIFIED | F-539 | The periodic spin-one Haldane gap | a finite component: the finite inputs of the two initializations — the trial MPS contractions at N = 72, 120 (exact U_N, V_N), the thermal recurrences (all nine t_{n,g} at b = 21/2 and W_{n,g} at b = 49/4 for n <= 12 recomputed exactly,… |
| CERTIFIED | F-540 | A boundary-field gap for the spin-one Heisenberg chain | a finite component: the fifteen thermal integers k_{n,g} recomputed by the printed recurrence and every enclosure built on them (Y_6 < .027, c_0 P_*(lambda_0)^2 < .003745), the four trial-vector certificates (m = 34, 78, 142, 240)… |
| CERTIFIED | F-541 | Uniform Stability of the Spherical Laughlin Gap | a finite component: this paper's restated seven-row certificate (Appendix A) — 13 three-body margins > 0 with the printed floors, M >= 0 exactly for D = 1..23 with the printed sign table, P^2 eta, 61/4096, 1222 and the final margin… |
| CERTIFIED | F-542 | A Fock-space inequality and the Laughlin spectral gap | a finite component: the seven published rows give the 13 three-body margins of eq:3certificate (all > 0, floors as printed) and the 23 four-body certificates of eq:4certificate (M >= 0 exactly, sign table as printed), each re-derived from… |
| CERTIFIED | F-549 | Entanglement with zero distillable secret key in local dimension ten | a finite component: the integer pencil and L (PPT), the twenty singular directions with every modular datum the paper prints, Phi_1 and Phi_2 PPT, Z PSD/PPT and nonzero with all twenty xhat x xhat in ker Z, rho = Z/tr Z in the class C,… |
| CERTIFIED | F-561 | Full support of the zero-temperature Sherrington-Kirkpatrick order parameter | a finite component: the exact rational certificate of Lemma cert:identity-lemma (the identity, every printed constant and the positivity of all 22 remainder coefficients) and the pointwise algebra of Lemma shape:ibp; not the sign lemmas,… |
| REFUSED | F-605 | The Kervaire invariant problem at the prime three | a finite component: the structure constants, the low-degree Ext groups D_{1,27} = <v^26 a, y, t_7'> and D_{6,10} = <v b^3> by an independent ordinary-cobar computation (matching the paper's printed checkpoints), the named cocycles and… |
| CERTIFIED | F-664 | Three fixed points on the symplectic quadric threefold | a finite component: f(x,y) = e.x + (x-p).y on S^2 x S^2 has exactly three critical points, q_0 = (p,-e) degenerate (Hessian rank 2); NOT the passage to Hamiltonian fixed points on Q^3 nor Crit(Q^3) = 4 |
| CERTIFIED | F-665 | Zero-Plane Rigidity for Einstein Four-Manifolds | a finite component: every exact polynomial certificate the paper prints -- the appendix lemmas scalar (8 interval boxes), matrix-and-boundary (12 triangle rows) and potential F (20 interval boxes), with the polynomials re-derived from… |
| CERTIFIED | F-667 | Positively curved Einstein four-manifolds | a finite component: every exact polynomial certificate the paper prints -- the appendix lemmas scalar (8 interval boxes), matrix-and-boundary (12 triangle rows) and potential F (20 interval boxes), with the polynomials re-derived from… |
| CERTIFIED | F-675 | A finite-time singularity of Calabi flow on projective space | the whole of Proposition cert:shoot (existence on [0,56], 1 + p > 0, |q| <= .25R, ||(Re xi, Im xi) - z*|| <= .13R for every z* in the square), by an independent validated integration; not the tail lemma, the matching or the theorem |
| CERTIFIED | F-678 | The Isoperimetric Conjecture for the Cubic Flat Three-Torus | a finite component: Proposition num:scalar-positive (B > 0 on [.64,1.02] u [1.62,2.25], B + S > 0 on [1.02,1.62]), decided independently, and the paper's knot and gap tables; NOT the geometric reduction to these inequalities |
| CERTIFIED | F-688 | A counterexample to integer-degree harmonic dimension comparison | a finite component: the supplementary exact spectral selection at n = 16, k = 50000 (finite-selection.tex) — every parameter inequality, the eigenvalue data, the multiplicities, every square-root bound and the three printed integers; not… |
| CERTIFIED | F-699 | The critical dimension for one-phase Bernoulli minimizers | a finite component: the exact arithmetic of Proposition cert:universal (the universal algebraic certificate behind the flatness half, d <= 6), from Tables I and II: the interior expansion with its 1714 keys and ten printed D_0 sums, D_0… |
| CERTIFIED | F-704 | Stable self-similar blowup for a supercritical defocusing Schrödinger equation… | a finite component: every finite comparison of Appendix cert:arithmetic (integer box, boundary-form positivity, winding sign table and margins, high-angular polynomial, profile enclosures and degree comparisons, exterior positivity), and… |