Evidence before headlines
Proof claim audit
18 recent claims with substantive supporting evidence, checked against their newest scope, final theorem, dependencies, formal assumptions, reproducibility, and independent mathematical reception. 5 currently clear the bar for an established result. Disputed, withdrawn, retracted, or materially incomplete artifacts are not listed on this site.
The decision rule
A build badge is not a proof.
The endpoint must match the advertised quantifiers and cannot depend on a decisive sorry, new axiom, black box, or unstated bridge. Machine checking is inspected at theorem level; conventional proofs require meaningful independent acceptance.
Grade C
13 claims · Clear filter
- CLAIM-004
Full subextremal Kerr exterior stability
Verification pendingGrade CExterior nonlinear stability for every fixed subextremal Kerr black hole, under the manuscript's regularity and asymptotic hypotheses.
Substantive full proof claim; not yet independently established.
Formal / reproducible check
A 333-page main proof and two public companion manuscripts exist; there is no formal proof.
Independent status evidence
No independent full technical audit, refereed acceptance, or second proof was located.
- CLAIM-012
Carathéodory umbilic conjecture
Verification pendingGrade CAt least two umbilics on every closed strictly convex C^(3,alpha) surface; this is not the canonical C^2 threshold.
Substantive higher-regularity full claim; independent acceptance remains pending and C^2 remains open.
Formal / reproducible check
No formalization. Three technical component papers are peer reviewed, but the complete synthesis remains an arXiv manuscript.
Independent status evidence
No independent line-by-line validation was located; recent third-party literature still treats the problem as a conjecture.
- CLAIM-014
High-dimensional Cohn–Elkies linear-programming exponent
Verification pendingGrade CThe exact exponential strength of the Cohn–Elkies linear program, a new sphere-packing upper exponent, and matching asymptotic Fourier sign-uncertainty constants.
Substantive same-day claim; even if correct, it improves an upper bound and a method limit rather than determining the true packing exponent.
Formal / reproducible check
The announcement says Lean certificates were released, but no pinned public certificate covering the full chapter was located and independently reproduced at the cutoff.
Independent status evidence
The 249-page bundled manuscript appeared on August 1, 2026; no independent end-to-end mathematical validation or refereed acceptance was located.
- CLAIM-015
Exponential improvements for binary and spherical code upper bounds
Verification pendingGrade CImproved asymptotic upper bounds by exponential factors for every fixed binary relative distance and spherical angle parameter.
Substantive progress claim pending verification; it does not settle either exact rate function or beat the binary Gilbert–Varshamov lower curve.
Formal / reproducible check
The announcement refers to machine-checked certificates, but a pinned, public, end-to-end certificate for all parameter ranges was not independently reproduced.
Independent status evidence
Only the same-day bundled manuscript and announcement were available at the cutoff; no independent technical audit was located.
- CLAIM-016
Explicit non-sofic group
Verification pendingGrade CThe explicit group \(L_{\mathbb F_2}(1,2)^\times\) is non-sofic, refuting the conjecture that every countable group is sofic.
Full-scope counterexample claim awaiting independent verification.
Formal / reproducible check
No pinned public formal endpoint or certificate for the group-theoretic reduction was independently reproduced at the cutoff.
Independent status evidence
The claim was announced with a same-day manuscript; no independent reconstruction, refereed treatment, or broad field acceptance was located.
- CLAIM-017
Counterexamples to Connes rigidity
Verification pendingGrade CInfinitely many pairwise nonisomorphic ICC property-(T) groups have isomorphic group von Neumann algebras.
Full-scope refutation claim awaiting independent verification.
Formal / reproducible check
No independently reproduced formal artifact establishes all group, factor, and nonisomorphism assertions.
Independent status evidence
The only full source located at cutoff was the same-day bundled manuscript; no independent operator-algebra audit was available.
- CLAIM-018
Permanent arithmetic-circuit and formula lower bounds
Verification pendingGrade CDivision-free circuits for the \(n\times n\) permanent require \(\Omega(n^2\log\log n)\) gates and formulas require \(\Omega(n^4/\log n)\) leaves.
Important lower-bound claim pending verification; the polynomial bounds do not imply \(VP\ne VNP\).
Formal / reproducible check
No independently reproduced proof-assistant endpoint or exact certificate covering the asymptotic lower-bound argument was located.
Independent status evidence
No independent complexity-theory validation was available on the manuscript's announcement date.
- CLAIM-019
General quantum parallel repetition
Verification pendingGrade CEvery finite two-player entangled game with value below one has exponentially decaying value under parallel repetition.
Full-scope theorem claim awaiting independent verification.
Formal / reproducible check
The announced Lean support was not available as a pinned public artifact that this audit could reproduce end to end.
Independent status evidence
No independent quantum-information reconstruction or refereed acceptance was located on the same-day cutoff.
- CLAIM-020
Fixed-polynomial-factor hardness of Euclidean CVP
Verification pendingGrade CA deterministic many-one reduction from 3SAT proves \(n^{1/400}\)-factor NP-hardness for Euclidean closest vector, with related nearest-codeword consequences.
Full target hardness claim awaiting independent verification.
Formal / reproducible check
No independently reproduced formal reduction or checked gap-preservation certificate was located.
Independent status evidence
The same-day manuscript had not yet received an independent lattice-complexity audit.
- CLAIM-021
Ehrhart sharp volume bound
Verification pendingGrade CEvery centered \(n\)-dimensional convex body with the origin as its only interior lattice point has volume at most \((n+1)^n/n!\); the equality classification is not claimed.
Sharp-inequality claim pending verification; the full catalog record remains open because equality is not classified.
Formal / reproducible check
No pinned public certificate for all dimensions was independently reproduced.
Independent status evidence
The bundled manuscript explicitly leaves equality open, and no independent verification of the inequality was located at cutoff.
- CLAIM-022
Multicolor triangle Ramsey growth
Verification pendingGrade CA superexponential lower bound matching the classical upper scale proves \(R_k(3)=k^{\Theta(k)}\).
Full asymptotic-order claim awaiting independent verification.
Formal / reproducible check
No pinned public formal certificate for the probabilistic and combinatorial estimates was independently reproduced.
Independent status evidence
No independent Ramsey-theory validation was located on the same-day announcement cutoff.
- CLAIM-023
Counterexample to Erdős–Simonovits compactness
Verification pendingGrade CA finite family of connected bipartite cyclic graphs has extremal number \(O(n^{4/3-1/48})\) although each member has extremal number \(\Omega(n^{4/3})\).
Full counterexample claim awaiting independent verification.
Formal / reproducible check
No independently reproduced certificate checks the finite forbidden family and all asymptotic estimates.
Independent status evidence
The construction was available only in the same-day bundled manuscript at the cutoff.
- CLAIM-024
Counterexample to Erdős's degeneracy conjecture
Verification pendingGrade CA fixed connected bipartite 2-degenerate graph \(H\) satisfies \(\operatorname{ex}(n,H)\ge c n^{3/2+\varepsilon}\).
Full counterexample claim awaiting independent verification.
Formal / reproducible check
No independently reproduced certificate verifies the graph construction, embedding exclusion, and lower bound.
Independent status evidence
No independent extremal-graph validation was available on the same-day cutoff.