Evidence before headlines
Proof claim audit
22 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.
All audited claims
22 claims
- CLAIM-001
Full Jacobian conjecture
EstablishedGrade AA counterexample in dimension 3, extended by identity coordinates to every dimension n >= 3.
Verified refutation for n >= 3; the plane case remains open.
Formal / reproducible check
Isabelle/HOL and Lean endpoints; the pinned Lean build was reproduced with no project sorry or custom axiom.
Independent status evidence
Exact rational recomputation and an independent expert reconstruction agree with the formal artifacts.
- CLAIM-002
Full Dixmier conjecture
EstablishedGrade AFailure at rank 3, hence at every rank n >= 3.
Verified refutation for ranks n >= 3; A1 and A2 remain open.
Formal / reproducible check
The decisive route is the published same-rank implication DC_n => JC_n plus the formally verified JC_3 counterexample.
Independent status evidence
An explicit A3 write-up passes exact algebra checks, but that script is corroboration rather than a proof-assistant formalization.
- CLAIM-003
Cycle Double Cover conjecture
EstablishedGrade AEvery finite loopless bridgeless multigraph has a cycle double cover.
Established theorem.
Formal / reproducible check
The unconditional Lean theorem cycleDoubleCover_of_bridgeless rebuilds at the pinned revision with no project sorry or added axiom.
Independent status evidence
Geelen and Oum reconstructed and explained the argument; Carmesin publicly confirmed it.
- 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-005
Thin-shell conjecture
EstablishedGrade BVar(|X|^2) <= Cn for every isotropic log-concave law in every dimension.
Established theorem.
Formal / reproducible check
Complete conventional proof at the exact standard scope; no proof-assistant formalization is claimed.
Independent status evidence
Field literature and an Oberwolfach report treat the result as the resolution of the conjecture.
- CLAIM-008
Consistency of New Foundations
Established · stated boundaryGrade BThe relative consistency implication Con(ZFC) => Con(NF).
Established relative result; the difficult TTT model is kernel-checked and the TTT-to-NF bridge remains a conventional paper proof.
Formal / reproducible check
The pinned ConNF build succeeds with no project sorry, admit, custom axiom, or unsafe; Lean proves the finite Hailperin axioms for the constructed TTT model.
Independent status evidence
The model-theory blueprint exposes the nonformalized bridge. The Stanford Encyclopedia reports the claimed relative result and its computer verification; it is status evidence, not an independent end-to-end reconstruction.
- 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.
- CLAIM-025
Complex structure on S^6
Verification pendingGrade CThe completed (3,4,infinity) modular family of complex two-tori is a compact complex threefold diffeomorphic to the smooth six-sphere, and therefore gives an integrable complex structure on S^6.
A substantive full existence claim is public, but it is not independently established.
Formal / reproducible check
The only located artifact is an unsigned, undated 108-page conventional manuscript hosted at alpo.ge; there is no proof-assistant development, pinned computational artifact, arXiv record, or refereed publication.
Independent status evidence
No independent end-to-end verification was located. The complex gluing and the final smooth-manifold recognition steps remain unaudited, and the document appeared immediately before this review.
- CLAIM-028
Whitehead asphericity conjecture
Verification pendingGrade CThe full classical integral assertion that every connected subcomplex of every aspherical two-dimensional CW complex is aspherical; Pasku and Kawauchi give separate affirmative claims.
Two full affirmative proof claims exist, but neither is independently established; the classical conjecture remains operationally open.
Formal / reproducible check
Both are conventional manuscripts with no formal or computational verification artifact. Pasku's 2021 preprint and Kawauchi's revised 2023–2024 manuscript/article use different presentation-theoretic and ribbon-link routes.
Independent status evidence
No independent reconstruction or mainstream refereed acceptance was located. A peer-reviewed 2025 paper proves only rational/prounipotent and pro-p analogues and explicitly continues to treat the classical integral problem as open.
- CLAIM-029
Positive sectional curvature on S^2 x S^2
Verification pendingGrade CThere exists a smooth Riemannian metric on S^2 x S^2 whose sectional curvature is strictly positive on every tangent two-plane.
A detailed full construction with executable symbolic calculations is public, but complete independent verification is still pending.
Formal / reproducible check
The Brendle-Hung arXiv v1 gives an explicit Cheeger deformation followed by a third-order perturbation and attaches a Mathematica notebook. There is no proof-assistant formalization or refereed publication, and the symbolic identities are essential to positivity.
Independent status evidence
A public third-party audit checked much of the geometric scaffolding and found a repairable parameter-bound mismatch, but explicitly imported rather than independently derived the ten decisive second-variation identities and one integral identity from the authors' notebook.
- CLAIM-030
Morrey 2x2 rank-one convexity problem
Verification pendingGrade CEvery finite-valued rank-one convex function f:R^{2x2}->R is quasiconvex.
A renewed full affirmative claim is available, but the 2x2 problem is not independently established.
Formal / reproducible check
Pedregal's manuscript is active as arXiv v5 (June 18, 2026) and gives a conventional fixed-point/H_n-condition proof, with no formal artifact. Version 3 was explicitly withdrawn in 2024 because some steps required a more transparent and convincing treatment; versions 4–5 reinstated a revised proof.
Independent status evidence
No independent reconstruction or refereed acceptance of the revised argument was located. The prior withdrawal materially raises the verification burden, while contemporary literature before the reinstatement continues to describe the planar problem as open.