Paper Watch tracks consequential new claims and translates the stakes: what could become possible if a result holds up, what we learn if it does not, and how close any real-world impact may be.
Listing is not validation. Every item is unexamined unless a separate proof docket records completed work. “Docket-ready” means a plausible check route is ready, not that the claim is true.
A paper analyzes which small disturbances of an idealized early-universe spacetime persist or grow in the linearized equations.
Who did it
Oliver Petersen
What it could mean
If the stated analysis holds, it sharpens a mathematical map of which modes matter near a singularity. It does not by itself describe our universe or settle the nonlinear Einstein equations.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the main theorem and definitions of the linearized variables, quasinormal modes, stability norm, and excluded self-similar modes; then check exactly how the Taub Bianchi-II linearization and the claimed no-symmetry conclusion follow. Do not execute manuscript artifacts.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract says the paper proves linear stability toward the Big Bang modulo an explicit finite-dimensional non-decaying self-similar space, then gives a complete linear description of the expected instability without symmetry assumptions. Because the title foregrounds instability while the first abstract sentence foregrounds stability modulo modes, the exact theorem statement and conventions are a required first check.
Why this could matter
Which ripples survive near a spacetime singularity? Kasner spacetimes are exact solutions used to study an extreme mathematical limit of gravity. This paper claims to sort their linear disturbances into decaying behavior and a finite set of persistent self-similar modes.
If it holds up
Foundational: it would give a sharper linear map for a difficult PDE-and-geometry regime, including the stated Taub-transition mode.
If it does not
The exact exceptional modes, stability norm, or linearization may need revision, clarifying where the proposed early-time picture stops applying.
a fresh, source-backed PDE/geometry theorem with a precise linearized scope. Intake does not resolve nonlinear Einstein evolution, establish a Big-Bang model, or verify the paper’s analysis.
Highest-risk dependency
The abstract’s stability-modulo-modes and instability language must not be flattened into either a nonlinear stability theorem or a general cosmological prediction. Gauge choice, norm, time direction, and the finite-dimensional exceptional space are load-bearing.
Available artifacts
arXiv exposes PDF, experimental HTML, and TeX source. The inspected record names no formal proof, code repository, numerical certificate, or executable artifact; AI involvement is not established.
Luisa Andreis, Riccardo W. Maffucci, and Federico Polito.
See the proposed checks
Inspect the exact transformations, invariants and inverse/reduction argument; verify the scope of pyramids, antibipyramids and facial four-cycles before treating the construction as complete.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract says two graph transformations generate every polyhedron other than pyramids from the square pyramid; it separately gives a unique-transformation construction for the specified facial-four-cycle sphere quadrangulations. It is a current constructive classification claim with a bounded combinatorial check surface.
Why this could matter
Two moves build many polyhedral graphs The work asks whether complex graph families can grow from one seed through a few reliable moves. Such recipes can make a large mathematical family easier to organize and explore.
If it holds up
The construction would provide a concise route to generate the stated non-exceptional polyhedra and related quadrangulations.
If it does not
An omitted graph family or failed inverse step would locate the limit of the proposed construction.
Impact horizon
Foundational · Graph theory · Combinatorics · Constructive mathematics
Version
submitted 2026-09-17 17:58:54 UTC
Why we tracked it
a fresh, source-backed constructive graph-theory result. The exact transformations, completeness argument and excluded classes remain unexamined.
Highest-risk dependency
A local transformation description does not establish completeness or uniqueness without the paper's reduction and exceptional-class argument.
Available artifacts
arXiv exposes PDF, experimental HTML and TeX source. No formal proof artifact, code repository, certificate or AI role is identified in the inspected record.
Inspect the main inequality and every boundedness hypothesis; then trace the stated reciprocal-estimate, signing-theorem and replica dependencies to the claimed Kadison–Singer consequence. Do not execute source artifacts for this intake.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract states a small-ball inequality for Boolean matrix series under bounded trace and variance conditions, then claims an interlacing-free proof of Kadison–Singer and further discrepancy corollaries. The explicit method and dependencies make the claimed advance an appropriate unexamined proof-method intake.
Why this could matter
A new route through matrix discrepancy The paper studies how random plus-or-minus choices can keep a matrix sum controlled. It offers a different proof mechanism for results about balancing many competing effects.
If it holds up
The method could give mathematicians another reusable way to derive matrix-balancing results and inspect which assumptions carry the work.
If it does not
Pinpointing a failed inequality or dependency would clarify which part of the proposed proof route cannot support its advertised consequences.
Impact horizon
Methods · Discrepancy theory · Matrix analysis · Proof methods
Version
submitted 2026-09-17 17:52:14 UTC
Why we tracked it
a fresh, source-backed discrepancy proof method with a stated main inequality and claimed consequence chain. Intake does not independently establish the inequality, its dependencies, or the asserted Kadison–Singer route.
Highest-risk dependency
The abstract-level consequence chain may conceal representation, normalization, or prerequisite assumptions; a new proof route does not by itself establish each advertised corollary.
Available artifacts
arXiv exposes PDF, experimental HTML and TeX source. The inspected source lists no formalization, code repository, certificate or replay package; AI involvement is not established.
A paper claims a weighted tree whose distances are exactly 1 through 153 cannot exist when it has 18 vertices.
Who did it
Maseeh Ghodsi
What it could mean
A finite graph puzzle can be impossible for reasons a computer helps expose. This work also makes the proof boundary visible: Lean checks some structure, while a separate search still needs its own scrutiny.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Source-lock the tagged artifacts; verify hashes and provenance; inspect the Lean declarations and axiom closure; then map the structural reduction to the separate computation/checker boundary. Any future execution must be isolated and must not silently turn a component replay into a whole-proof verdict.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract claims that no Leech tree of order 18 exists. It says Lean 4 verifies structural facts reducing a putative example to eight local configurations; conventional mathematics establishes an exact-cover condition and search completeness; exhaustive computation closes the eight cases. The source explicitly calls this a computer-assisted proof rather than an end-to-end Lean formalization.
Why this could matter
When a proof has both a kernel and a search Can one weighted tree realize every whole-number distance from 1 through 153 exactly once? This paper says no—and carefully divides its evidence between Lean-checked reductions and an exhaustive search.
If it holds up
Methods: it would resolve this finite graph puzzle while offering a candid map of what a proof kernel certifies and what remains in the computation-and-checker trust boundary.
If it does not
The split record helps locate the problem: a formal reduction, a conventional argument, the search program, its run, or the checker may need correction.
Impact horizon
Methods · Graph theory · Computer-assisted proof · Formal verification
Version
submitted 2026-09-17 14:41:05 UTC
Why we tracked it
a fresh computer-assisted finite nonexistence claim with a clearly stated formal/computational boundary. Intake is not an end-to-end proof validation or an independent reproduction.
Highest-risk dependency
Kernel checking of the structural layer does not certify the unformalized search, its execution, or the theorem-to-artifact correspondence. Conversely, a gap in the computational layer would not automatically negate every formal structural fact.
Available artifacts
The arXiv record links a version-v1.0.0 Lean artifact, a version-v1.0.0 computational-evidence release, and an earlier Zenodo preprint. The source expressly says the search program, its execution, and certificate checker are not formalized in Lean. No artifact was downloaded, executed, or replayed.
A paper claims that a 27-by-27 square is the smallest square tileable by integer rectangles no two of which contain one another in both dimensions.
Who did it
George M. Georgiou
What it could mean
An apparently tiny tiling puzzle can hide a hard impossibility proof. If this holds, every smaller square is ruled out—and the public search records show exactly where finite checking enters the argument.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
First source-lock and hash-check the ancillary release, then examination the structural reduction from the theorem to the finite candidate list. Any dual-implementation replay belongs in a separate isolated environment and must compare its output to the stated 167,538 count and exact (n,k) scope.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract claims that for every integer (nleq26) and every number of tiles (kgeq2), the (n× n) square has no tiling by pairwise incomparable integer rectangles, establishing that the known 27-by-27 example is smallest. Its finite stage is reported to search 167,538 candidates using two independently written programs.
Why this could matter
Why 26-by-26 may be forever too small Cut a square into integer-sided rectangles, but forbid any rectangle from being at least as wide and tall as another. A 27-by-27 example is known; this paper claims every smaller square is impossible.
If it holds up
Foundational: it would close a clean finite geometry puzzle and show how structural reasoning can shrink an enormous search to a checkable set of cases.
If it does not
A missing tile family, an incomplete reduction, or a mismatched search record would show exactly where the claimed impossibility needs repair.
a fresh finite combinatorial theorem with public dual-implementation evidence artifacts. Intake does not mean the finite search, logs, checksums, or theorem correspondence have been independently replayed.
Highest-risk dependency
Finite enumeration supports only the candidate universe reached by the structural reductions. A successful rerun would not establish the theorem if the reduction omits a permitted rectangle family, changes incomparability conventions, or mismatches the stated quantifiers.
Available artifacts
arXiv lists a complete ancillary verification package with two implementations, build instructions, SHA256SUMS, C/Python source, output logs, and certificate/round-trip logs. No source, log, checksum, or program was downloaded, executed, or replayed.
A paper claims an online algorithm can choose a strong feasible set even when options appear one by one.
Who did it
Hamed Abdi, Kiarash Banihashem, MohammadTaghi Hajiaghayi, and Danny Mittal
What it could mean
Choosing now can mean missing the best offer that arrives later. If this holds, it gives a sharp guarantee for making good choices under a specific mathematical kind of constraint—not every real-world marketplace.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Hamed Abdi, Kiarash Banihashem, MohammadTaghi Hajiaghayi, and Danny Mittal.
See the proposed checks
Inspect the exact theorem statements and define their arrival-order, value, representation, and oracle assumptions; verify that the linear-matroid 1/e theorem is not conflated with the separate arbitrary-matroid prophet or 1/64 reduction claims. No code needs to be run for this first source review.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract claims a 1/e-competitive ordinal secretary algorithm for every linear matroid, maintaining expected-intersection-dimension bounds while selecting online. It separately claims a 1/2 single-sample prophet algorithm for arbitrary matroids and a black-box 1/64 secretary reduction. This is a newly posted, concrete advance on structured online selection, not a blanket result for all allocation problems.
Why this could matter
How do you choose before every offer arrives? Hiring, booking, and bidding all share a cruel timing problem: accept too early and a better option may appear; wait too long and nothing remains. This paper claims a sharp online-selection rule for a structured family of feasible choices.
If it holds up
Enabling: it would settle the strong secretary guarantee for linear matroids, giving algorithm designers a precise benchmark for online selection under that structure.
If it does not
The sharp guarantee or its scope would need revision, revealing which arrival, independence, or representation assumption carries more weight than claimed.
a fresh, source-backed online-selection theorem with a precise claimed guarantee. Intake is not a verification of the algorithm, its constants, or an application to any operational allocation problem.
Highest-risk dependency
A linear-matroid feasible set is not automatically a real capacity, pricing, authority, or lifecycle model. The guarantee's online-information and representation assumptions determine what it says; a claimed 1/e result does not make it an all-purpose offer-selection rule.
Available artifacts
arXiv exposes PDF, experimental HTML, and TeX source. The inspected primary record identifies no Lean/Rocq/Coq/Isabelle development, code repository, certificate, or replay package. AI involvement is not established by this source.
A theorem claims a proposed kind of Navier–Stokes singularity cannot occur when its forcing is spatially real analytic.
Who did it
Peter Constantin, Mihaela Ignatova, and Vlad Vicol
What it could mean
How a fluid is driven matters. Under specified symmetry and scaling assumptions, analytic forces rule out blowup. OpenAI’s construction uses non-analytic forcing, so this is a boundary, not a refutation.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Peter Constantin, Mihaela Ignatova, and Vlad Vicol.
See the proposed checks
examination Theorem 1.3’s force regularity, anisotropic-bound, and axisymmetric-core assumptions; compare them line by line with the cited OpenAI manuscript’s Theorem 1.1 and Appendix-A properties; then review the ancient-limit and local-regularity argument without executing manuscript code.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract and Theorem 1.3 claim regularity for a specified class of forced 3D Navier–Stokes solutions. As a consequence, a singular construction with the named core and anisotropic properties cannot have force that both remains (C²)-bounded to singular time and is locally uniformly real analytic in space. It is a timely mathematical boundary on the September 8 forced Navier–Stokes intake, not a refutation of that claim.
Why this could matter
A sharp new boundary around a fluid singularity claim Navier–Stokes singularities are notoriously hard to rule in or out. This paper says a particular proposed route cannot work with a force that remains real analytic in space, narrowing the terrain without resolving every case.
If it holds up
Foundational: it would impose a concrete regularity constraint on this class of forced singularity constructions and focus scrutiny on the exact behavior of their forcing.
If it does not
The proposed restriction would weaken, revealing which symmetry, scale, or analyticity step needs a more careful argument.
a fresh, source-backed conditional regularity theorem materially constraining an active forced Navier–Stokes claim. It does not by itself decide the OpenAI construction, whose forcing need not meet the theorem’s analytic hypothesis.
Highest-risk dependency
The consequence is conditional. Equating smooth compactly supported forcing with real-analytic forcing, or treating this theorem as a general no-blowup result, would overstate its scope.
Available artifacts
arXiv exposes PDF, HTML, and TeX source. The primary record did not identify a formal proof, code repository, numerical certificate, or executable artifact. No artifact was downloaded, executed, or replayed.
A paper claims new frequency sets that can reconstruct every signal in broad classes, with the main statements formalized in Lean.
Who did it
Susanna Bertolini, Enric Florit-Simon, Lukas Liehr, and Mitchell A. Taylor
What it could mean
Fourier analysis asks what samples retain enough information to recover a signal. If the formalization matches the paper, it offers both new constructions and a machine-checkable route through delicate analytic claims.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Susanna Bertolini, Enric Florit-Simon, Lukas Liehr, and Mitchell A. Taylor.
See the proposed checks
In a separate ephemeral environment, source-lock the cited repository and toolchain, reproduce the five declarations and inspect their axiom closure; then compare the formal statements with Theorems 1.1–1.4 and the stated (L^p), density, and measurability hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract claims uniformly discrete density-one frequency sets complete in every (L^p(S)) for (|S|<1), density-(v) integer-frequency counterparts for (|S|<v), and sharpness of a Sobolev threshold. Section 7 describes a Lean formalization of the results. This is a newly posted mathematical result that also makes its checking boundary inspectable.
Why this could matter
New frequency sets aim to capture every signal A signal can be rebuilt from frequencies only when they carry enough information. This paper proposes unusual sparse-looking sets that still capture every function in stated classes, then records key claims in Lean for machines to check.
If it holds up
Methods: the constructions would extend the map of when frequency samples determine a function, while the formalization supplies a reusable example of checking advanced analysis with software.
If it does not
A replay or alignment examination would isolate whether the frequency construction, analytic assumptions, or formal statement is too strong.
a fresh analysis result with a public Lean formalization. The primary source reports compilation, but State of Proof has not replayed the package or checked paper-to-Lean correspondence.
Highest-risk dependency
A compiling endpoint can establish only its exact formal declarations and trusted axioms; it does not automatically establish that every analytic hypothesis, novelty claim, or prose conclusion in the paper is represented.
Available artifacts
The arXiv record links UniversalCompleteness; Section 7 states that five public Lean theorems compile under Lean 4.31.0. No repository was downloaded, executed, or replayed.
A paper and Lean package claim every finite 3-connected plane graph has a convex drawing that supports greedy routing.
Who did it
Lech Mazur, with ProofAtlas-reported contributions from OpenAI Codex and OpenAI GPT-6 Pro
What it could mean
A long-standing graph-drawing question may gain an exact machine-checkable endpoint, while the crucial comparison between that code and the companion paper remains open.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Lech Mazur (paper author and accountable editor); ProofAtlas reports source roles for OpenAI Codex and OpenAI GPT-6 Pro in computation, formalization, and proof strategy.
See the proposed checks
In a separate ephemeral environment, source-lock the disclosed Lean commit; reproduce its build and unfinished-proof/axiom checks; then independently compare the formal theorem’s original-drawing hypotheses and conclusion with the companion paper’s stated strong conjecture.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The exact declaration constructs a straight-line embedding with strict convex face cycles and a neighboring vertex closer to every distinct destination, under an original-drawing and deletion-connectivity formulation of finite simple 3-connected plane graphs.
Why this could matter
A route through every planar network may become greedy In a greedy drawing, each hop toward a destination gets strictly closer. This release claims every sufficiently well-connected planar network can be drawn that way, while keeping the proof’s exact scope and independent review visible.
If it holds up
It would settle the stated strong graph-drawing conjecture and provide a formal endpoint for studying convex greedy-routing constructions.
If it does not
A mismatch between the Lean statement, its assumptions, or the paper’s claimed theorem would identify the boundary needing repair; the conjecture would remain open.
Impact horizon
Methods · Graph theory · Computational geometry · Formal verification
Version
public version of 2026-09-09; companion paper is 15 pages; Lean package reports 499 first-party files and a pinned build evidence record.
Why we tracked it
This older-than-72-hours release was newly surfaced by the current Reddit discovery channel and independently inspected at its primary formalization page. It supplies both a precise theorem declaration and explicit limits rather than a social claim alone.
Highest-risk dependency
Lean verification applies to the exact declaration, not automatically to every sentence of the paper or its historical claim. The source explicitly leaves paper-to-statement alignment, independent replication, specialist review, and accepted-result status open.
Available artifacts
ProofAtlas exposes a public pinned Lean source package, a checker-evidence JSON record, a source ZIP, a main Lean file, and the companion PDF. No manuscript, source package, or checker was downloaded, executed, or replayed.
Elias De Jesús (repository maintainer; commits credit Claude Opus 5 for portions of the September 13 formalization work).
See the proposed checks
In a separate ephemeral environment, pin commit 20fda6e, inspect the declared trust boundary and run the owning Lean targets; then compare the exact statement of harmonicapdiscrepancy with the README’s prose and verify that no conditional interface is silently used.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The current source declares Lean formalizations of finite residue-count and harmonic arithmetic-progression discrepancy bounds, plus cylinder arithmetic. Its documentation explicitly limits these to finite or conditional infrastructure and states that the Collatz conjecture and the project’s Global Occupation Conjecture remain open.
Why this could matter
Small Collatz lemmas become machine-checkable Collatz research involves patterns in repeated odd-number transformations. This revision formalizes finite rules for how evenly certain residue classes appear, including a harmonic-weighted version, while explicitly not claiming to solve the famous conjecture.
If it holds up
It would add reusable machine-checkable building blocks and clearer boundaries between finite arithmetic facts, conditional arguments, and open questions.
If it does not
A declaration, dependency, or claimed scope boundary would need repair; the open Collatz problem remains open.
Impact horizon
Methods · Number theory · Formal verification · Dynamical systems
Version
main commit 20fda6ebf2c1d13b07fb64d339a55595ebeb242f, pushed 2026-09-13 11:56:27 UTC; adds harmonic packing and 8/9-drift-exclusion formalization after a same-day cylinder next-digit-counting revision.
Why we tracked it
The primary artifact was substantively revised today and supplies inspectable theorem declarations rather than an unsupported general Collatz claim. It is a bounded example of how a research program exposes exact claims and stated non-claims for machine checking.
Highest-risk dependency
A successful Lean build would establish only the declarations under its toolchain and axioms; it would not establish manuscript novelty, any bridge from finite discrepancy to real Collatz trajectories, EOC, or Collatz itself.
Available artifacts
Public Lean 4 repository with pinned toolchain and Mathlib manifest. The source labels its listed declarations “FORMALLY VERIFIED,” but no artifact was downloaded, built, or replayed here.
Source-lock the manuscript; reconstruct the stated closed zero-dimensional graph, then verify local finiteness, the no-Borel-unfriendly-partition argument, and the precise bounded-degree positive cases against the cited question and definitions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract says the author constructs a closed, unbounded-degree locally finite Borel graph with no Borel unfriendly partition, answering Thomas's question negatively. It also states positive bounded-degree cases. A named-question counterexample released within the current intake window merits a clearly bounded public examination route.
Why this could matter
An infinite network resists a fair-looking split An unfriendly partition puts each vertex with at least as many opposite-side neighbors as same-side neighbors. This paper claims a carefully structured infinite graph where no Borel, or systematically describable, partition can do that.
If it holds up
It would settle Thomas's Borel-graph question negatively and sharpen the boundary between finite-style graph intuition and measurable infinite structures.
If it does not
The proposed graph, its local finiteness, or the measurability obstruction would need repair; the question would remain open.
Impact horizon
Foundational · Graph theory · Descriptive set theory · Combinatorics
Version
submitted 2026-09-10 17:57:55 UTC
Why we tracked it
a fresh, source-backed counterexample to a named Borel-graph question, with a stated structural construction and no linked machine-checkable artifact; intake is not validation.
Highest-risk dependency
The construction's descriptive-set-theoretic regularity and the quantifiers in "Borel unfriendly partition" are central; an informal graph construction or a different measurability class would not establish the stated negative answer.
Available artifacts
arXiv provides PDF, experimental HTML and TeX source for a 13-page manuscript. The abstract page does not identify a Lean, Coq, Isabelle, code, data or certificate artifact. No manuscript artifact was downloaded, executed or replayed.
Extract the proposed five-qubit gate; independently verify its fifth-level Clifford-hierarchy membership, exhaust the claimed generalised-semi-Clifford normal form obstruction, and test the inverse-closure consequence using the paper's definitions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The abstract claims a five-qubit gate in the fifth Clifford-hierarchy level that is not generalised semi-Clifford, refuting the Zeng-Chen-Chuang conjecture and showing the hierarchy is not closed under inverses. It is a newly posted concrete counterexample to a named structural conjecture.
Why this could matter
A five-qubit gate breaks a tidy hierarchy rule Quantum gates can be sorted into layers of increasing complexity. This paper claims one five-qubit gate in the fifth layer cannot be reshaped into the simple form a long-standing conjecture predicted.
If it holds up
It would refute the generalized semi-Clifford conjecture and show the Clifford hierarchy is not closed under taking inverses.
If it does not
The gate's layer membership or the claimed normal-form obstruction would need correction; the conjecture would remain unsettled.
Impact horizon
Foundational · Quantum information · Algebra · Mathematical physics
Version
submitted 2026-09-10 17:55:10 UTC
Why we tracked it
a fresh, source-backed counterexample to a 2007 quantum-information conjecture; the abstract supplies the claimed object but no independently replayable artifact, so the result remains unexamined intake.
Highest-risk dependency
The counterexample turns on exact conventions for the hierarchy and the normal form; a gate representation, phase convention or membership proof that differs from the paper's definitions could invalidate the claimed refutation.
Available artifacts
arXiv provides PDF, experimental HTML and TeX source; the page labels it a preliminary draft. No linked formalization, circuit repository, executable verification package, data or certificate artifact was identified. No artifact was downloaded, executed or replayed.
The paper claims a Lean proof that no strongly regular graph with parameters (266, 45, 0, 9) exists.
Who did it
Kay Akiyama
What it could mean
Some perfectly balanced networks may be impossible to build, however long you search. This proof could rule out one elusive pattern with a computer-checkable argument instead of a giant search certificate.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Obtain the archive in a separate ephemeral environment; check its release hash/dependencies, compile the public root with Lean, independently run the stated checker, and examination the arXiv theorem-to-formal-statement correspondence.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper claims there is no strongly regular graph with parameters ((266,45,0,9)), via a classification-free Lean proof that reduces the remaining case to an impossible projection identity. It is a current example of formal proof construction without external infeasibility certificates.
Why this could matter
A stubborn graph pattern may be impossible Strongly regular graphs are highly symmetric networks with exact local rules. This paper claims one long-sought parameter set cannot exist, using a Lean formalization that follows the contradiction through lattice and design arguments rather than an external infeasibility certificate.
If it holds up
It would close this specific existence question and supply a formally checkable example of a classification-free nonexistence proof.
If it does not
The parameter translation, lattice argument, or formal statement may need repair; the graph’s existence question would remain open.
Impact horizon
Methods · Combinatorics · Formal verification · Graph theory
Version
submitted 2026-09-08 06:43:09 UTC
Why we tracked it
a fresh finite nonexistence claim with an archived Lean 4 formalization and an explicit independent nanoda check claim; not independently replayed.
Highest-risk dependency
The high-level combinatorial claim depends on exact parameter and theorem-statement correspondence; a successful checker run would not establish that the prose claim has been modeled without omission.
Available artifacts
arXiv links a Zenodo Lean 4 formalization archive and states the theorem uses standard Lean axioms and was also checked with nanoda. No artifact was downloaded, executed, or replayed.
The paper states conditions for copying database rows while live changes continue, without losing, reviving, or overwriting newer data.
Who did it
Andreas Andreakis
What it could mean
Imagine moving a database while everyone keeps editing it. This work could help engineers prevent old data overwriting new data—or deleted records coming back from the dead.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
In an isolated environment, reproduce the stated artifact build/check routes; then map one DBLog watermark and stale-copy rule to its exact source/target state model and test that the formal endpoint covers all claimed protocol variants.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper states conditions under which a chunked database copy can be interleaved with an active change log without gaps, stale copied state overwriting newer logged updates, or deletion resurrection; it covers multiple DBLog/Debezium/Flink/back-up variants. This is a directly inspectable new proof-method result for committed-state handoff and reconciliation.
Why this could matter
Copying live data without losing the plot A database copy can collide with updates still arriving from the live system. This paper claims conditions that prevent missed changes, stale overwrites, and deleted rows returning during that handoff across several change-data-capture designs.
If it holds up
It would provide a verified foundation for reasoning about copy-to-log handoffs, including watermarking and related capture designs.
If it does not
One or more stated conditions or protocol variants may be incomplete, narrowing where the claimed reconstruction guarantee applies.
Impact horizon
Enabling · Databases · Distributed systems · Formal verification
Version
submitted 2026-09-08 02:44:49 UTC
Why we tracked it
a fresh formal-methods paper with a concrete commitment/reconciliation theorem, stated Isabelle/HOL, Lean 4, and TLA+ evidence routes, and source-linked artifacts; not independently replayed.
Highest-risk dependency
The paper’s state/reconciliation assumptions may not match a real provider’s authority, idempotency, ordering or unknown-outcome semantics. A formal database theorem cannot itself attest to an external reservation or commitment side effect.
Available artifacts
arXiv links a Zenodo formal-verification release; the abstract claims the complete theory is machine-checked in Isabelle/HOL, its core independently verified in Lean 4, and protocols bounded-model-checked in TLA+. No artifact was downloaded, executed, or replayed.
A reported Lean formalization establishes a positive lower density of starting values reaching 1 within logarithmically many ordinary Collatz steps.
Who did it
Lech Mazur, developed with AI agents through ProofAtlas
What it could mean
A simple number game has resisted mathematicians for decades. This does not solve Collatz, but it could prove that a definite share of starting numbers reach the finish line quickly.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Lech Mazur; developed with AI agents through ProofAtlas (the release credits OpenAI Codex for computation, formalization, proof strategy, and exposition).
See the proposed checks
Obtain the released source only in a separate ephemeral environment; verify dependency pins, public-root axioms and the exact theorem declaration; then examination the source-to-paper correspondence, explicit constants, cutoff, and the claimed ordinary-step convention.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The release claims fixed explicit constants (c>0) and (X₀) such that every (X≥ X₀) has at least (cX) positive starts (n<X) reaching 1 within ((523/50)ln n) ordinary Collatz steps. It expressly does not resolve the full Collatz conjecture. The source is consequential both as a partial result and as a current AI-assisted formalization package.
Why this could matter
A real fraction reaches 1 quickly The Collatz puzzle asks whether every positive integer eventually reaches 1 under a simple rule. This release claims something narrower: a fixed positive fraction reach 1 within a logarithmic number of ordinary steps, beyond a very large cutoff.
If it holds up
It would give number theory an explicit positive-density result with a checkable formal endpoint, while leaving the full Collatz conjecture open.
If it does not
The formal statement, constants, cutoff, or source-to-paper alignment would need correction; the full conjecture remains unresolved either way.
Impact horizon
Foundational · Number theory · Dynamical systems · Formal verification
a newly released, explicitly scoped Collatz partial result with a declared Lean source package, successful owning-target build transcript, and a bounded replay route; inclusion is not independent validation.
Highest-risk dependency
The release’s build and artifact claims are publisher assertions until independently replayed. Positive lower density with an enormous cutoff is not density-one convergence, an optimal bound, or a solution of Collatz.
Available artifacts
The primary release links a theorem-specific Lean source package, pinned dependencies, recorded no-sorry/axiom checks and a successful owning-target build transcript. No artifact was downloaded, executed, or replayed in this intake.
The paper reports a proof that smooth, forced three-dimensional Navier–Stokes flow can break down in finite time.
Who did it
OpenAI
What it could mean
Weather forecasts. Aircraft wings. Blood flow. Fluid equations underpin all three. This claim could expose a breaking point in forced, three-dimensional Navier–Stokes—even when the fluid starts perfectly still.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Map the exact paper and Lean endpoints to Clay alternatives C and D, including force regularity, initial data, energy and periodic pressure; then perform an isolated formal replay with pinned external checker tools.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Fluid moves inward around the axis and escapes along it. In the paper’s proposed construction, the active core becomes narrower as its speed grows. The drawing illustrates that mechanism; it is not a computed solution.
OpenAI claims a finite-time breakdown of smooth, forced, three-dimensional incompressible Navier–Stokes flow from rest with bounded energy, asserting alternatives C and D of the Clay problem. This is the publisher's claim, not a State of Proof validation.
Why this could matter
Navier–Stokes: can fluid equations hit a breaking point? Wings, weather and blood flow all involve fluid equations. OpenAI claims that even smooth inputs can drive one idealized model beyond smooth behavior. This concerns the model's limits—not instantly better aircraft or forecasts.
If it holds up
It would resolve the forced breakdown alternatives of the Clay problem and sharpen research into when smooth fluid models stop applying.
If it does not
A gap would identify which assumption or proof step needs repair; ordinary engineering uses would not automatically become invalid.
Public manuscript retrieved 2026-09-08; PDF SHA-256 0e779481c4da40bd28d1e642e1d8ca57447d129610df28dfa5a11e9af8ae228f. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
Whether the formal statement matches the complete manuscript and official Clay assumptions remains unassessed. Formal replay and expert review have not been performed by State of Proof.
Available artifacts
A public formal-source repository is linked: https://github.com/openai/NavierStokesAndEuler/tree/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538. OpenAI attributes the work to an internal AI-agent system. No manuscript-linked code was executed; source availability is not proof verification.
The paper presents AI-guided evidence and a proposed route toward a stable singularity in ideal fluid flow.
Who did it
Adarsh Ganeshram, Valentin Duruisseaux, and Anima Anandkumar
What it could mean
An AI may have spotted the mathematical moment a smooth fluid model breaks. Finishing the proof would turn that machine-found pattern into something researchers can actually rely on.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
The manuscript presents evidence of a stable finite-time singularity, an approximate profile discovered with a physics-informed neural network, and a framework reducing nonlinear stability to finite quantitative estimates.
Why this could matter
AI finds a candidate; completing the proof comes next A neural network finds an approximate pattern that could become a singularity in ideal fluid flow. The manuscript offers evidence and a stability framework, but explicitly lists unfinished proof work. Finding a promising pattern is not yet proving it exists.
If it holds up
Completing the quantitative certification could turn AI-guided discovery into a rigorous singularity result under the exact stated assumptions.
If it does not
An unsuccessful certification would reveal where the approximate pattern or stability estimates need to change.
Public manuscript retrieved 2026-09-08; PDF SHA-256 f0164c40fad09a646412acec95f7908ea6b2fd61d16b809954a4048665fb5f78. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
The manuscript explicitly lists remaining work to complete the proof. Do not label this a completed Euler solution or equate partial certification with the full theorem.
Available artifacts
No formal replay artifact was established in this bounded intake. A physics-informed neural network is central to profile discovery. The paper limits the role of language models to supporting tasks. No manuscript-linked code was executed; source availability is not proof verification.
The paper claims a smooth-forcing breakdown result for an idealized porous-flow model.
Who did it
Levent Alpöge, Tristan Buckmaster, and Matei P. Coiculescu
What it could mean
Water through rock seems gentle. Its mathematics may not be. This result would show smooth forcing creating infinitely sharp changes in an idealized porous-flow model—revealing a hidden limit of that description.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Periodic incompressible porous media · two dimensions
∂ₜρ + u(ρ) · ∇ρ = F; ∇ · u(ρ) = 0
The arrows and lines suggest flow through pores; the color change suggests variation in density. In the equation, ρ is density and u(ρ) is its Darcy velocity. The porous material illustrates the physical idea; the paper studies a continuum model with periodic boundaries, not this pore geometry. The picture is not simulation data.
The paper claims finite-time density- and velocity-gradient blowup for a periodic incompressible porous-media model with smooth initial density and a force smooth in space and time.
Why this could matter
Fluid through a sponge hides a difficult mathematical limit Think of water seeping through a sponge. This idealized porous-flow model asks how sharply density and velocity can vary under smooth inputs. Its value is understanding mathematical limits, not a demonstrated improvement to groundwater prediction.
If it holds up
It would extend a known singularity construction to forcing smooth in both space and time within the stated periodic model.
If it does not
It would expose the step that fails to preserve time smoothness or the claimed gradient growth.
Public manuscript retrieved 2026-09-08; PDF SHA-256 b3ebdbb8d9a93dcca5f3b3f8796e63f7f28b48e0b0e258b909110a4b69c72a12. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
A periodic idealized model, not a physical reservoir experiment. We have not assessed the proof or established a paper-to-formal correspondence.
Available artifacts
A public formal-source repository is linked: https://github.com/tristanbuckmaster/fluidlean. The paper says Claude helped recover elements of prior work and Claude/Codex assisted writing and bookkeeping under the authors' direction. No manuscript-linked code was executed; source availability is not proof verification.
The paper claims that smooth, unforced three-dimensional ideal-fluid flow can develop a finite-time breakdown.
Who did it
OpenAI
What it could mean
Even a frictionless, unforced fluid model could tie its own mathematics in knots. A verified result would show smooth motion breaking down without an outside shove.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Each stage adds a localized oscillation to a background flow. In the paper’s construction, one stage helps amplify the next, producing increasingly large gradients. The panels illustrate the idea; they are not computed snapshots.
The paper claims finite-time breakdown for smooth, compactly supported initial flow in the three-dimensional unforced incompressible Euler equations.
Why this could matter
Can an ideal fluid break down without an outside push? Take friction and external pushing out of the picture. Can a smooth ideal flow still develop unbounded gradients? This paper claims it can, probing a fundamental limit of the equations used to understand fluid motion.
If it holds up
It would establish a smooth-data, whole-space breakdown example for unforced Euler, changing the mathematical picture of ideal-fluid regularity.
If it does not
The proposed construction would need repair; the general smooth-data question would not be settled by this argument.
Public manuscript retrieved 2026-09-08; PDF SHA-256 a0c234518e6c489e16996805023eb2e75c00b7c03455f7a3a5be2c124954bfdd. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
A separate unforced Euler claim, not the forced Navier–Stokes claim. No proof execution or semantic correspondence review by us.
Available artifacts
A public formal-source repository is linked: https://github.com/openai/NavierStokesAndEuler. OpenAI attributes the result to a coordinating AI-agent system and provides a Lean formalization. No manuscript-linked code was executed; source availability is not proof verification.
The paper claims smooth forcing can produce unbounded twisting and gradients in three-dimensional ideal-fluid flow.
Who did it
Levent Alpöge and Tristan Buckmaster
What it could mean
A smooth push does not necessarily mean a smooth ride. This claim would show an ideal fluid model developing unbounded twisting under smoothly applied forces—not real water reaching infinite speed.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
The paper claims finite-time blowup of vorticity and circulation gradients in three-dimensional incompressible Euler flow with a force smooth in space and time, including at the terminal time.
Why this could matter
A smooth push can still produce extreme fluid structure A smoothly applied force need not keep an ideal fluid smooth forever. The authors claim a flow whose twisting and gradients become unbounded. This is about a mathematical limit, not proof that real water reaches infinite speed.
If it holds up
It would strengthen our understanding of singularity formation under smooth forcing and provide a construction to study related equations.
If it does not
A failed estimate or translation would locate what must be repaired before relying on the claimed smooth-forcing result.
Public manuscript retrieved 2026-09-08; PDF SHA-256 97ef408bff09b4f6ed9f3867734d1eb2245f3f34e6334b28136c84c02d0ae8d8. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
Forced Euler, not unforced Euler or Navier–Stokes. The authors report formal verification; State of Proof has not replayed it. Authorship follows the authors' statement; the inspected Euler PDF has no byline on its first page.
Available artifacts
A public formal-source repository is linked: https://github.com/tristanbuckmaster/fluidlean. The authors describe extensive Claude and Codex assistance within a human-directed program building on Córdoba and Martínez-Zoroa. No manuscript-linked code was executed; source availability is not proof verification.
The paper claims a finite-time singularity in a simplified two-dimensional buoyancy-flow model with smooth forcing.
Who did it
Levent Alpöge and Tristan Buckmaster
What it could mean
No runaway heat required. Smooth forcing could drive temperature changes across tiny distances beyond any bound, while temperatures themselves stay finite—a striking breakdown in the mathematics of warm fluid rising through cooler fluid.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
∂ₜθ + u · ∇θ = fθ; ∂ₜu + (u · ∇)u + ∇p = θe₂ + fᵤ; ∇ · u = 0
Warm and cool contours represent the temperature anomaly θ. Closer contours mean a sharper change across a smaller distance. The paper claims that temperature stays bounded while its gradient grows without bound, using a sequence of finer oscillatory layers and smooth forcing. This is a schematic of that distinction, not a computed temperature field.
The paper claims finite-time singularity formation in the two-dimensional inviscid Boussinesq system with smooth forcing, bounded temperature, and unbounded temperature gradient and vorticity.
Why this could matter
Warm rises, cold sinks—and the mathematics gets sharper Buoyancy helps warm fluid rise through cooler fluid. This simplified model asks whether smooth inputs can create arbitrarily fine structure while temperature remains bounded. The result could clarify the model's limits, not directly improve tomorrow's forecast.
If it holds up
It would establish a precise breakdown mechanism for a forced, two-dimensional buoyancy model and support further mathematical study.
If it does not
The claimed forcing or stability argument would need repair; it would not invalidate every buoyancy model.
Public manuscript retrieved 2026-09-08; PDF SHA-256 895a628d1783bcb039374686f50b895b5f450f53b8ef8aa173523487a7a4a21b. Discovery date is not a claim of first publication.
Why we tracked it
The September 8 fluid-mathematics announcements warrant distinct intake records for each equation, forcing assumption and proof-completion state.
Highest-risk dependency
A forced, inviscid two-dimensional model. Not a result about all weather models. Formal and mathematical review by us remain pending.
Available artifacts
A public formal-source repository is linked: https://github.com/tristanbuckmaster/fluidlean. The shared authors' statement describes LLM-assisted work extending the Córdoba–Martínez-Zoroa program. No manuscript-linked code was executed; source availability is not proof verification.
The paper claims a dense-network rule forcing every large tree shape, alongside a result on multicolor tree patterns.
Who did it
Bruce Reed and Maya Stein
What it could mean
Add enough connections and a network loses the freedom to avoid certain branching patterns. This claimed threshold would turn ‘surely it must be there’ into a mathematical guarantee for large, dense networks.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Source-lock the TeX bundle; independently reconstruct the dense decomposition and tree-embedding argument with all parameter dependencies; verify the threshold and sufficiently-large-(n) quantifiers; then separately trace the claimed reduction to the multicolor Ramsey consequence with specialist extremal-combinatorics review.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims that for every (gamma), all sufficiently large (n)-vertex graphs with more than ((k-2)n/2) edges contain every (k)-vertex tree whenever (k≥gamma n). It also claims to solve a 51-year-old Erdős-Graham problem on multicolor Ramsey numbers of trees. This is a current, high-consequence partial-regime resolution of a landmark extremal-graph question.
Why this could matter
Dense networks must contain every tree shape A dense network cannot avoid a chosen branching pattern forever. This paper claims the exact edge threshold forces every large tree shape to appear, settling the dense regime of a major extremal-graph question.
If it holds up
It would give combinatorics a sharp dense-network embedding rule and resolve a long-standing multicolor Ramsey question about trees.
If it does not
The exact threshold or asymptotic range needs repair, preventing premature use as a universal dense-graph guarantee.
Impact horizon
Foundational · Graph theory · Combinatorics · Network structure
Version
submitted 2026-09-04 17:59:54 UTC
Why we tracked it
a fresh claimed resolution of the dense-regime Erdős-Sós conjecture, with a second named consequence, but no linked formalization, codebase, or certificate artifact; no docket created.
Highest-risk dependency
The load-bearing risk is quantifier and constant management across the asymptotic dense-regime embedding theorem. The abstract does not expose whether the decomposition, absorption, or regularity-type steps preserve the exact ((k-2)n/2) threshold and the stated (k≥gamma n) range.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source. The primary abstract page lists no source-linked Lean, Coq, Isabelle, code repository, data, or certificate artifact. No manuscript artifact was downloaded or run.
The paper claims a broad family of hyperbolic symmetries reduces to three seed shapes.
Who did it
Daniel Allcock, Pat Devlin, Anna Felikson, Alex Kontorovich, and Ian Whitehead
What it could mean
Just three building blocks could organize a sprawling family of hyperbolic shapes. That would turn an intimidating geometric wilderness into a map researchers can actually use.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Daniel Allcock; Pat Devlin; Anna Felikson; Alex Kontorovich; Ian Whitehead.
See the proposed checks
Source-lock the TeX bundle; independently verify arithmeticity and commensurability invariants for the three seed polyhedra; reconstruct the gluing classification for ideal right-angled cases; then trace the reduction from the Koebe-Andreev-Thurston correspondence to the stated conjecture with specialist hyperbolic-geometry review.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper claims that every arithmetic reflection group arising from a combinatorial polyhedron is commensurable to one arising from a tetrahedron, square pyramid, or cuboctahedron, proving the Kontorovich-Nakamura conjecture. Its stated intermediate theorem classifies arithmetic ideal right-angled hyperbolic polyhedra as gluings of three seed polyhedra.
Why this could matter
Infinite hyperbolic symmetries reduce to three seeds Hyperbolic polyhedra can encode vast families of geometric symmetries. This paper claims every arithmetic case in one major construction descends from just three building blocks, turning a classification puzzle into a finite map.
If it holds up
It would organize a broad class of arithmetic reflection groups around three seed geometries, enabling sharper classification work.
If it does not
The proposed seeds may not cover every case, exposing where arithmeticity or gluing arguments need stronger conditions.
Impact horizon
Foundational · Hyperbolic geometry · Number theory · Symmetry
Version
submitted 2026-09-04 16:57:28 UTC
Why we tracked it
a fresh claimed proof of the 2016 Kontorovich-Nakamura conjecture on arithmetic hyperbolic reflection groups, with an explicit structural reduction but no linked formalization, codebase, or certificate artifact; no docket created.
Highest-risk dependency
The crucial issue is whether the proposed gluing classification is exhaustive and preserves the arithmetic and commensurability conditions needed for the original reflection-group statement. The abstract does not expose exceptional polyhedra, field hypotheses, or the reduction's treatment of non-ideal cases.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source; the abstract page notes 39 pages and 24 figures. No source-linked formal proof, executable code, data, or certificate repository was found. No manuscript artifact was downloaded or run.
The paper claims two conjectured families of counting polynomials have only real roots, using links among several combinatorial structures.
Who did it
Per Alexandersson
What it could mean
Apparently different puzzles—parking arrangements, words, and noncrossing patterns—could share hidden mathematical order. Proving these connections would let mathematicians carry insights from one counting problem into another.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Source-lock the TeX bundle; formalize the stated bijection from tieless parking functions to finite-alphabet Smirnov words; independently derive the last-letter interlacing recurrence and its common-interlacer consequence; then check the two conjecture statements and every specialization against their original definitions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper claims real-rootedness for Chow polynomials of noncrossing partition lattices and proves Conjecture 4.2 of Xiao and Conjecture 11.2 of Ehrenborg-Hetyei-Readdy. It presents interlacing, differential-recurrence, and finite Schur-Szegő-convolution routes, making a current assertion suitable for targeted review.
Why this could matter
Hidden polynomial patterns keep their roots orderly Many counting problems produce polynomials whose roots reveal deep regularity. This paper claims two conjectured families have only real roots, using new translations between parking functions, words, and noncrossing structures.
If it holds up
It would settle two combinatorial real-rootedness conjectures and add reusable interlacing tools for structured counting polynomials.
If it does not
The claimed translation or recurrence would need narrowing, preserving caution around predicted root behavior in these families.
Impact horizon
Foundational · Enumerative combinatorics · Algebraic combinatorics · Polynomial theory
Version
submitted 2026-09-04 13:31:37 UTC
Why we tracked it
a fresh claimed resolution of two named real-rootedness conjectures in algebraic and enumerative combinatorics, with multiple proof routes stated but no linked formalization, codebase, or certificate artifact; no docket created.
Highest-risk dependency
The key risk is whether the recurrence preserves all combinatorial weights and boundary cases needed to transfer real-rootedness back to the exact Chow and toric (g)-polynomials. The claimed equivalence to the two named conjectures must also be checked against their original normalizations.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source; the abstract page notes 18 pages and invites comments. No source-linked Lean, Coq, Isabelle, executable code, data, or certificate repository was found. No manuscript artifact was downloaded or run.
The paper claims that finitely many same-sign point charges have only finitely many electric-field balance points.
Who did it
Alberto Enciso and Daniel Peralta-Salas
What it could mean
Invisible electric forces can balance at surprising places. This result would rule out endlessly many balance points from finitely many same-sign charges—closing a question that has resisted mathematicians since 1969.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Source-lock the TeX bundle; reconstruct the complex-curve reduction and the proof excluding equilibrium curves for same-sign charges; independently verify the hypotheses of the Bézout count and derive the stated mixed-sign bound; then obtain specialist review of the algebraic-geometry and complex-analysis steps.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims that finitely many same-sign point charges in three-dimensional space generate an electric field with only finitely many equilibria, answering a 1969 question of Morse and Cairns. It also states an explicit bound for mixed-sign charges away from the zero set of an auxiliary function. A current resolution claim with a bounded algebraic-geometric core warrants prompt, non-validating intake.
Why this could matter
A 1969 question about electric balance points may close Point charges create invisible push-and-pull fields. This paper claims that any finite collection with one charge sign has only finitely many balance points, ending a decades-old question and making their global geometry less mysterious.
If it holds up
Foundational: mathematicians gain a firm finiteness rule for same-sign Coulomb fields and an explicit counting framework for more complicated mixed-sign arrangements.
If it does not
The old question remains open, and the failure would reveal where the complex-curve or algebraic counting argument overreaches.
Impact horizon
Foundational · Mathematical physics · Dynamical systems · Algebraic geometry
Version
submitted 2026-09-03 15:00:22 UTC
Why we tracked it
a fresh claimed resolution of a named 1969 finiteness question, with an explicit quantitative extension and a clear specialist-review route but no linked formalization, codebase, or certificate artifact; no docket created.
Highest-risk dependency
The decisive issue is whether the complex-curve argument rules out every positive-dimensional equilibrium component under the stated real and singularity conditions before Bézout is applied. The mixed-sign statement also depends on restricting to the complement of the auxiliary function’s zero set.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source. No source-linked formal proof, executable code, data, or certificate repository was listed on the primary record. No manuscript artifact was downloaded or run.
The paper reports AI-agent-assisted formal verification of an xv6 operating-system kernel down to RISC-V hardware semantics.
Who did it
M. Frans Kaashoek and Nickolai Zeldovich
What it could mean
Could your next computer ship with fewer hidden bugs? This teaching-kernel project points toward AI-assisted proofs that, if the approach scales, could catch low-level mistakes before software reaches real devices.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Obtain a source-pinned MachCSL/Iris/Sail/xv6 artifact if released; identify the exact xv6 and Sail revisions; replay the stated verification with proof-assistant kernel checks; map the 6,593-line scope and each reported bug to the specification; and independently examination hardware-model, concurrency, DMA, and agent-generated-proof trust boundaries.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The layers connect kernel code, memory resources and processor behavior. MachCSL extends separation-logic reasoning to detailed RISC-V execution, including behavior below a single instruction. The illustration explains the levels involved; it is not an actual chip layout or a verification result.
The authors introduce MachCSL, adapting Iris-style concurrent separation logic to Sail RISC-V sub-instruction semantics, and report an AI-agent-assisted verification of a 6,593-line xv6 kernel implementation that found nine xv6 bugs and one Sail-semantics bug. It squarely tests whether LLM agents can contribute to reviewable low-level formal verification while the source is current.
Why this could matter
AI-assisted proofs reach down to computer hardware Operating systems make devices usable, but their deepest rules must survive memory, interrupts, and hardware translation. This paper claims AI agents helped verify a real teaching kernel at that level, while uncovering implementation and specification bugs.
If it holds up
Methods: it would offer a concrete model for combining formal hardware semantics, human-designed invariants, and machine assistance in reviewable systems verification; reuse elsewhere still requires released artifacts and independent replay.
If it does not
The claimed verification scope or bug findings would narrow, showing which model, proof boundary, or AI-produced step needs stronger evidence before such workflows are trusted.
Impact horizon
Methods · Formal verification · Operating systems · AI-assisted proof
Version
submitted 2026-09-03 16:17:47 UTC
Why we tracked it
a fresh, unusually consequential AI-assisted formal-methods claim with specific reported scope and bug findings, but no source-linked repository, proof scripts, or independently replayable artifact on the primary record; no docket created.
Highest-risk dependency
The abstract does not identify the proof assistant, the released proof objects, the exact source revisions, the nine kernel bugs, or how agent output was checked. Without those artifacts, the claimed coverage, bug findings, and reliability of the AI-assisted proof workflow are not independently assessable.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source. No public repository, proof-assistant project, version-pinned script, proof object, or bug-fix set is linked on the primary record at retrieval. No artifact was downloaded or executed.
A reported Lean formalization turns the known proof of Fermat’s Last Theorem into steps a computer can check.
Who did it
Anthropic’s Claude agents, with research led by Tianyi Peng
What it could mean
Fermat is already proved. Imagine giving that proof a ‘verify’ button. If this scales, AI-assisted mathematics could arrive with independently checkable logic—catching errors before other research builds on them.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Anthropic; named research lead Tianyi Peng; Lean sources produced by Claude agents.
See the proposed checks
In an isolated high-memory environment, clone the exact source commit; verify source hashes and provenance; run the default lake build; run verification/comparator/run.sh against the Mathlib-only challenge; run verification/nanoda/run.sh; inspect the four nanoda performance patches; and have a formal-methods reviewer map PROOF-PATH.md and the encoded theorem to the intended Frey–Serre–Ribet–Wiles/Taylor-Wiles argument.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
aⁿ + bⁿ ≠ cⁿ for positive integers a, b, c and integer n > 2
Each tile stands for a mathematical statement; the connections show which earlier statements it depends on. The announcement describes a dependency graph used to organize a Lean formalization of Fermat’s Last Theorem. This illustration explains that structure; it is not the project’s actual proof graph.
Anthropic reports that Claude agents produced in eleven days the first complete end-to-end, computer-checked Lean proof of Fermat's Last Theorem. This is not a new solution to an open problem—Wiles and Taylor-Wiles proved the theorem in 1995—but a claim that their known mathematical route has been rebuilt as a fully machine-checkable formal artifact at unprecedented scale and speed.
Why this could matter
A landmark proof becomes software machines can check Fermat's Last Theorem was solved in 1995. The new achievement is different: turning that enormous human proof into code independent computers can replay. If this scales, AI-generated mathematics can arrive with a checkable receipt—helping researchers find errors and spend time understanding the truth.
If it holds up
A reproducible end-to-end Lean proof would show that AI can help turn landmark mathematics into independently checkable software, making formal verification a practical companion to human peer review as mathematical output accelerates.
If it does not
Fermat's theorem remains proved, but this artifact would not yet demonstrate a reliable new route for machine-checking large AI-assisted proofs; the verification workflow would need repair.
Impact horizon
Methods · Formal verification · AI mathematics · Research infrastructure
Version
Anthropic research announcement, published 2026-09-04; public proof repository pinned at unsigned commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef, authored 2026-09-03
Why we tracked it
Anthropic's complete Lean 4 formalization claim is pinned to a public source commit with three concrete replay routes; it remains source-locked and independently unvalidated by State of Proof, and no docket has been created.
Highest-risk dependency
The evidence is author-supplied and the repository's formalization.yaml labels review status self-assessed with no listed reviewers. Full replay is resource-heavy—the published route reports hundreds of gigabytes of working storage and up to roughly 300 GB of memory—and machine checking establishes formal inference, not by itself the semantic faithfulness of every named intermediate result or generated explanation.
Available artifacts
The pinned Apache-2.0 repository contains roughly 13 million lines of Lean, 29,511 theorem/proof modules, FinalCheck.lean, a human-readable PROOF-PATH.md, metadata declaring zero sorry terms and exactly Lean's three standard axioms, a Lean Comparator challenge, and an independent nanoda-kernel replay route. Lean 4.33.1 and Mathlib commit db584cd6d46c92f209a44c0f1c829460d327499d are pinned. The artifact builds on and attributes work from the Imperial College London FLT project, flt-regular, and Mathlib.
The paper claims a proof that Catalan's constant cannot be expressed as a ratio of whole numbers.
Who did it
Zhi-Wei Sun
What it could mean
We can compute this number to astonishing precision and still not know whether it is a fraction. This claim would finally answer that basic question—and might unlock methods for other mysterious constants.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
In a separate ephemeral sandbox, source-lock the TeX bundle; translate the stated weighted constructions into independently derived exact rational linear forms in (1) and (G); verify integrality/denominator bounds and the required asymptotic decay; then obtain specialist number-theory review of the limiting irrationality criterion.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims that Catalan's constant (G=sumkgeq0(-1)^k/(2k+1)²) is irrational, presenting this as a proof via suitable weights. Irrationality of (G) is a long-standing open problem, so the first primary v1 merits prompt, explicitly non-validating intake.
Why this could matter
A famous constant may finally leave mathematical limbo Mathematicians can calculate Catalan's constant to enormous precision but still do not know whether it is a ratio of whole numbers. Settling that basic identity question could reveal new ways to prove that familiar constants are fundamentally non-fractional.
If it holds up
Foundational: it closes a famous open problem and may supply reusable techniques for proving other constants irrational; it does not imply an immediate new device or speedup.
If it does not
The failure identifies where a promising weighted-series argument loses the arithmetic or asymptotic control needed to prove irrationality.
Impact horizon
Foundational · Number theory · Mathematical constants · Proof verification
Version
submitted 2026-09-03 17:55:12 UTC
Why we tracked it
a fresh claimed resolution of a long-standing number-theory question, with a precise primary source and a plausible proof-review route but no linked formalization, codebase, or certificate artifact; no docket created.
Highest-risk dependency
The decisive risk is whether the proposed weights simultaneously establish nonzero integer (or controlled-denominator) linear forms and decay strong enough to force irrationality. A formal manipulation of the displayed series alone would not establish the required arithmetic and asymptotic bounds.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source. No source-linked formal proof, executable code, data, or certificate repository was found on the primary record. No manuscript artifact was downloaded or run.
The paper claims a highly symmetric graph disproves a proposed 1998 bound on network coverage resilience.
Who did it
Prateek R. Srivastava
What it could mean
Picture a network watched by as few guards as possible. This claimed counterexample breaks a long-standing rule about how many connections must fail before extra guards are needed.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
In a separate ephemeral sandbox, source-lock the archive; independently reconstruct the truncated-octahedral graph; verify planarity, cubicity, and domination number 8; enumerate all four-edge deletions with a separately implemented exact checker; then compare results with both supplied verifiers.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper claims that the planar cubic truncated-octahedral graph has domination number 8 and bondage number 5, giving (5>Delta(T)+1=4) and therefore a counterexample to the stated 1998 planar-graph conjecture. Its finite verification reportedly covers all 58,905 four-edge sets.
Why this could matter
One tiny graph may overturn a 28-year-old prediction A 1998 conjecture proposed a limit on how easily coverage can break in certain networks. This paper says a familiar, highly symmetric graph exceeds it. The mathematics can inform coverage models, but practical effects would be indirect.
If it holds up
Foundational: researchers must replace the conjectured bound and rethink this corner of graph robustness before drawing broader lessons for coverage or fault-tolerance models.
If it does not
The 1998 bound survives this test, and the exhaustive check should reveal whether the graph, deletions, or domination count was encoded incorrectly.
Impact horizon
Foundational · Graph theory · Network robustness · Exhaustive verification
Version
submitted 2026-09-02 11:48:23 UTC
Why we tracked it
a fresh, finite claimed counterexample with source-archived independent C++20 and Python verifiers and a bounded exhaustive replay route; no docket created.
Highest-risk dependency
The decisive risk is faithful graph encoding and exhaustive enumeration: a missing or duplicated edge-set branch, or a mistaken domination convention after deletion, could alter the claimed bondage number.
Available artifacts
The arXiv record says its TeX source archive contains a complete C++20 verifier and an independently written Python verifier. Those artifacts were not downloaded or executed in this automation.
The paper claims a smooth surface mesh can have a global dimensional defect invisible to local checks.
Who did it
Xinyu Wu and Jiansong Deng
What it could mean
A smooth-looking digital surface can hide a mathematical trap. This result could reveal why local mesh checks miss whole-shape dependencies—relevant to the mathematics behind CAD, animation, and simulation.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Extract the 18-triangle coordinates and (t=1/5) specialization; independently form the smoothing-cofactor and Bernstein--Bézier matrices over exact rationals; verify their ranks and that every interior four-star is nonsingular; then compare the resulting dimension with the stated lower bound.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims a nondegenerate planar 18-triangle complex at (t=1/5) where (dim S¹₃(mathcal T)=34) exceeds Schumaker's predicted lower bound 33 despite no singular interior four-star, refuting the conjectured sufficiency of the local correction (sigma).
Why this could matter
Curved digital surfaces have hidden global dependencies Splines are the smooth patches behind computer-aided design, animation, and numerical simulation. This paper says checking each local mesh neighborhood can miss a dependency created by the geometry of the whole surface.
If it holds up
Enabling: spline software and mathematical models may need global checks, helping prevent silent dimension errors in CAD, surface design, and simulation pipelines.
If it does not
The classical local correction may still be sufficient; the unusual extra degree of freedom would trace to a rank or geometry calculation error.
Impact horizon
Enabling · CAD and geometry · Numerical simulation · Spline theory
Version
submitted 2026-09-02 10:43:50 UTC
Why we tracked it
a fresh, explicit counterexample to the proposed universal attainment of Schumaker's lower bound, with a tightly specified 18-triangle family but no replay artifact on the primary record.
Highest-risk dependency
The counterexample requires that the coordinate specialization remains nondegenerate and that both rank calculations use exactly the same spline-space constraints; a numerical rank claim alone would not settle either condition.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source; no linked code, exact matrix data, formal proof, or certificate repository was found on the primary record.
The paper claims an infinite three-dimensional grid walk with no three visited points in a line.
Who did it
Stijn Cambie and Erik Kalviainen
What it could mean
Walk forever on a three-dimensional grid without ever lining up three visited points. A verified construction would solve that astonishing puzzle using finite rules a computer can check.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
In a separate ephemeral sandbox, inspect the pinned Lean theorem statements, imports, and axiom/trust-base report; map the sixteen-vector periodic or inductive construction in the manuscript to those statements; then independently check the finite no-three-collinear kernel and the inference to the infinite walk.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims an infinite walk in (ℤ³), using a fixed set of sixteen step vectors, whose vertices contain no collinear triple—answering the Gerver--Ramsey problem popularized as Erdős Problem 193. It is unusually ready for source-to-formal scope mapping because the arXiv record links both a Lean/formal project and a public project surface.
Why this could matter
An infinite walk that never lines up three points The construction solves a deceptively simple puzzle: move forever through a 3-D integer grid without ever placing three visited points on one line. It is also a compact test of machine-checked mathematics.
If it holds up
Foundational: it closes Erdős Problem 193 and supplies a reusable blueprint for formally verified infinite constructions built from finite, checkable rules.
If it does not
The puzzle remains open, while the mismatch would teach us where a finite checker or Lean statement failed to cover the infinite walk.
a current claimed resolution of Erdős Problem 193 with a source-linked Lean 4 formalization, exact finite checks, and a separately inspectable public project; no docket created.
Highest-risk dependency
The core scope risk is whether the formal statement covers the whole infinite construction rather than only its finite kernel, and whether the manuscript's no-collinearity convention precisely matches the encoded predicate.
Available artifacts
The primary record explicitly links Lean 4 formalization, exact finite checks, and an interactive visualization. No artifact was run in this automation.
The paper claims to establish Albertson's conjecture for graphs needing up to 26 colors.
Who did it
Ankan Sadhu
What it could mean
Some networks are simply too tangled to draw neatly. This result would extend a precise link between coloring complexity and unavoidable crossings through 26 colors—not solve every possible case.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Reconstruct the reduction to the stated three residual orders from cited published results; independently verify each finite/order-specific crossing-number inequality and the appendix's reproof of the (19≤ rleq24) range; then assess the claimed (r=27) structural corollary separately.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper claims that every graph with chromatic number (r≤ 26) has crossing number at least that of (Kr), extending the previously reported (rleq24) range by resolving the remaining orders for (r=25,26). The paper also states a constrained structural consequence for a hypothetical (r=27) exception.
Why this could matter
How much tangling does complex connectivity force? When a network needs many colors to separate conflicting connections, must it also require many crossings when drawn? Settling more cases sharpens the boundary between abstract connectivity and unavoidable geometric congestion.
If it holds up
Foundational: Albertson's conjecture is established through 26 colors, extending the known frontier by two cases and sharply restricting a possible 27-color counterexample.
If it does not
The 25- and 26-color cases remain unproved by this argument; failure would not itself produce a counterexample or show that the conjecture becomes false below 27.
a fresh extension of a named graph-theory conjecture through two remaining chromatic-number cases, but with no source-linked formalization, codebase, or certificate artifact.
Highest-risk dependency
The extension hinges on the exact hypotheses and completeness of the cited reductions for (r=25,26); the compact abstract cannot establish that the three residual cases exhaust all critical graph orders.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source; no linked formal proof, code, data, or certificate repository was found on the primary record.
The paper claims no universal algorithm can decide integer solvability for every polynomial equation in ten unknowns.
Who did it
Zhi-Wei Sun
What it could mean
Not every problem yields to a bigger computer. If this holds, even equations with ten unknowns admit no algorithm that can always decide whether an integer solution exists.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Map the new ten-variable construction against the cited eleven-variable theorem; verify the Diophantine encoding and variable count at each reduction; then review the undecidability transfer and coefficient-domain conditions independently.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims that no algorithm decides integer solvability for arbitrary polynomial equations in ten unknowns, improving the previously stated eleven-unknown result. It is a specific advance on a restricted-variable form of Hilbert's tenth problem, not a new resolution of the original 1970 undecidability result.
Why this could matter
Some ten-variable equations can defeat every algorithm This is a hard limit on computation, not merely a slow-algorithm result. It says no universal program—not even a future AI—can always decide whether an integer polynomial with ten unknowns has a solution.
If it holds up
Foundational: it moves undecidability from eleven variables to ten, tightening our map of problems that computation can never solve in full generality.
If it does not
The known eleven-variable impossibility remains; the attempted compression identifies where an undecidability encoding needs an extra variable.
Impact horizon
Foundational · Computability · Number theory · AI limits
Version
submitted 2026-09-01 17:56:48 UTC
Why we tracked it
a fresh improvement to a sharp undecidability-variable bound for a foundational problem, but without a supplied replay or formal-verification artifact.
Highest-risk dependency
The claimed variable reduction is load-bearing: auxiliary parameters or quantifier/encoding conventions must not silently add variables or weaken the universal integer-coefficient formulation.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source; no linked formal proof, code, data, or certificate repository was found on the primary record.
The paper claims a classification of exact integer partitions into Beatty sequences: whole-number patterns produced by a rounding rule.
Who did it
Hu Tan and Ying Zhang
What it could mean
Imagine several rhythms covering every beat exactly once, with no collisions. This claim would settle which proportions make that perfect fit possible in a famous family of mathematical sequences.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
State the precise periodic/common-period reduction; independently verify the inverse-sine obstruction and each claimed finite rational/integer verification; then examination the induction and two-sequence disjointness step that converts the one-third-density assertion into the full binary scale pattern.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims Fraenkel's conjectured binary density pattern for partitions of the integers into at least three Beatty sequences with distinct moduli. Its proposed route runs through a dimension-free one-third-density statement, Fourier cancellation, and three exact finite verifications, making the proof architecture specific enough to map promptly.
Why this could matter
Perfectly interlocking number schedules may have one shape Imagine several repeating schedules that cover every integer exactly once without collision. Fraenkel's conjecture says that, with three or more distinct rhythms, their shares must follow one rigid doubling pattern.
If it holds up
Foundational: a decades-old classification becomes complete, deepening the mathematics of exact partitions and potentially informing future work on collision-free periodic scheduling.
If it does not
Other perfectly balanced patterns may exist, and the failed step would narrow where to search for them.
Impact horizon
Foundational · Number patterns · Discrete scheduling · Exact partitions
Version
submitted 2026-09-01 17:36:33 UTC
Why we tracked it
a fresh full-resolution claim for a named number-theory conjecture, but without a public formalization, codebase, or certificate route on the primary record.
Highest-risk dependency
The dimension-free reduction and its use of the three finite verifications must cover every allowed number of Beatty components and preserve the distinct-moduli hypotheses; the abstract cannot establish that global scope.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source; no linked formal proof, code, data, or certificate repository was found on the primary record.
The paper reports three curves with 144 shared tangent circles, exceeding a previously proposed maximum of 136.
Who did it
Taylor Brysiewicz
What it could mean
Three curves. 144 circles touching all three. If the construction checks out, it breaks the supposed ceiling of 136—and gives geometric solvers a tougher test of what they can find.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Extract the three conic equations and proposed circle data; use exact or certified interval algebra to verify tangency and realness, deduplicate circles, and confirm the count of 144; separately inspect the definition and provenance of the superseded 136 maximum.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript exhibits three conics with 144 real tritangent circles, exceeding and thereby contradicting the conjectured maximum of 136. The finite claimed witness makes this a comparatively bounded algebraic-geometry intake target.
Why this could matter
Geometry has more tangent circles than we thought Three simple curves can share far more tangent circles than the previous proposed ceiling allowed: 144 instead of 136. That changes the landscape for a classic geometry-counting problem.
If it holds up
Enabling: geometric solvers and enumerative methods gain a tougher benchmark, improving how researchers count and certify all real solutions to tangency constraints.
If it does not
The 136 ceiling may survive; the examination would expose duplicated, non-real, or merely approximate circles.
a fresh, concrete counterexample to a stated extremal maximum, with a bounded numerical/algebraic verification route but no primary-record certificate artifact.
Highest-risk dependency
Numerical presentation alone can conceal multiplicity, non-real branches, or repeated solutions; the check must establish that 144 distinct real circles satisfy all three tangency conditions under the exact stated conics.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source; no linked formal proof, code, coordinates, or certificate repository was found on the primary record.
The paper claims a quantified gap between two ways of grouping a random network, with a linked formalization of one consequence.
Who did it
Samuil Petkov
What it could mean
Let groups be fully connected or fully disconnected, and a random network can be organized more economically. This claim would put a precise lower bound on how large that advantage becomes.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Clone the pinned formal commit; rebuild under its pinned Lean/Mathlib toolchain; inspect the theorem statement and axiom examination; then separately map the manuscript's signed-overlap/second-moment derivation to the formal theorem hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims to resolve Erdős and Gimbel's question by showing, along the full sequence for (Gn ∼ G(n,1/2)), that (χ(Gn)-ζ(Gn)) exceeds an explicit positive multiple of (n/(log n)³) with probability tending to one. It is unusually timely because the author supplies a Lean 4 formalization of the explicit full-sequence lower-bound consequence and a public replay archive, while disclosing AI-assisted development.
Why this could matter
Random networks hide a real shortcut in their structure A random network can be grouped more efficiently when groups may be either fully connected or fully disconnected than when only independent groups are allowed. The paper quantifies that advantage at scale.
If it holds up
Foundational: it resolves an Erdős–Gimbel question and gives researchers a sharper baseline for random-graph partitioning and average-case combinatorial optimization.
If it does not
The claimed full-sequence gap is not established; the failure would identify where a probabilistic or formally encoded bound overreaches.
Impact horizon
Foundational · Random networks · Graph partitioning · Probability
Version
submitted 2026-08-31 11:18:17 UTC
Why we tracked it
a current claimed resolution of Erdős–Gimbel Problem 625 with a narrowly scoped, version-pinned Lean 4 statement and public clean-replay record. The source lock and formal-artifact scope are sufficient to prepare a docket; neither settles the manuscript-only phase-refinement claims.
Highest-risk dependency
Kernel checking establishes only the encoded formal statement relative to the stated Lean trust base. The load-bearing issue for the paper is whether the formal statement faithfully captures all hypotheses and whether the manuscript-only phase-resolved refinement follows from the written probability argument.
Available artifacts
The source cites the exact Lean/replay archive revision, whose recorded formal-source commit is 824e4b609466d2e26b216a76ecf103184dac2663. The archive exposes Lean sources, axiom examination, checksums, logs, and a clean-environment replay. The manuscript explicitly limits the formalization to the stated full-sequence coefficient, not its phase-resolved refinement.
The paper claims a counterexample showing a proposed condition cannot guarantee convergence for a Fourier-averaging process.
Who did it
Ushangi Goginava
What it could mean
Averaging is supposed to calm things down. This counterexample would show a proposed Fourier-averaging rule going wildly wrong even at a well-behaved point—a warning for the mathematics behind signal reconstruction.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Extract the proposed sequence and function; establish convexity, the growth bound, and the Lebesgue-point property independently; then reproduce the lower-bound/divergence estimate for the arithmetic means.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The paper claims that the Carleson–Trigub–Zagorodniĭ logarithmic-growth condition is not sufficient for Belinsky's 1997 conjecture: it constructs a strictly convex increasing sequence ((am)) with (am≤ 7m⁸) and an (L¹(𝕋)) function for which the specified Cesàro means are unbounded at a Lebesgue point.
Why this could matter
A long-standing Fourier averaging test may fail Fourier averaging is a mathematical way to tame unstable wave reconstructions. This counterexample says a long-standing condition still cannot guarantee convergence at a locally well-behaved point; consequences for practical signal and image methods would be indirect and long-term.
If it holds up
Foundational: analysts must strengthen a proposed convergence test and gain a precise counterexample for building a correct replacement.
If it does not
The sufficiency claim may survive; the proposed sequence or function fails one of the required growth, convexity, or local-regularity conditions.
Impact horizon
Foundational · Harmonic analysis · Signal reconstruction · Convergence guarantees
Version
submitted 2026-08-31 10:48:49 UTC
Why we tracked it
fresh, narrowly stated refutation of the sufficiency direction of a named Fourier-analysis conjecture, but with no linked formal or computational replay artifact.
Highest-risk dependency
The construction must satisfy all three constraints simultaneously—strict convexity, the polynomial upper bound, and unbounded Cesàro behavior at the stated Lebesgue point. The abstract does not expose the quantitative estimate coupling them.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source; no linked formal proof, code, data, or certificate repository was found.
The paper claims smooth log-concave distributions can violate a proposed entropy pattern.
Who did it
Jiayang Zou, Luyao Fan, Jiayang Gao, and Jia Wang
What it could mean
Even beautifully smooth probability curves can break an elegant rule about how uncertainty spreads. These claimed counterexamples would tell information theorists exactly which tempting shortcut they cannot trust.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Jiayang Zou, Luyao Fan, Jiayang Gao, and Jia Wang.
See the proposed checks
Re-derive the two-frequency circular entropy calculation with exact/symbolic or interval arithmetic; examination the Gaussian-windowed heat-flow transfer; then verify that strict log-concavity and the sign persistence survive the localization and tensorization steps.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The authors claim smooth, strictly log-concave examples in every dimension that violate Gaussian complete monotonicity; in dimension one, the claimed explicit family has a negative signed (m)-th entropy derivative for every sufficiently large (m), persisting for small positive time. The manuscript states that GPT-5.6 Sol Pro developed the proof under author guidance, making the source particularly relevant to the AI-assisted-proof watch lane.
Why this could matter
A supposed universal law of entropy breaks Entropy tracks how uncertainty spreads under heat-like smoothing, a core idea in probability and information theory. This AI-assisted proof claims a broad family of beautifully behaved distributions still violates the expected pattern.
If it holds up
Foundational: researchers lose a proposed universal shortcut for entropy inequalities and gain explicit stress tests for future theorems in information theory and probability.
If it does not
The conjecture survives, and the error would pinpoint whether the AI-assisted periodic calculation, real-line transfer, or tensorization went wrong.
Impact horizon
Foundational · Information theory · Entropy · AI-assisted proof
Version
submitted 2026-08-31 05:40:52 UTC
Why we tracked it
fresh explicit counterexample family to a named Gaussian-inequality conjecture, with an explicit AI-development disclosure but no supplied formal or executable certificate artifact.
Highest-risk dependency
The analytical bridge from the periodic calculation to the real-line heat-flow construction, and the all-dimension tensorization argument, are the load-bearing steps; an explicit family does not by itself expose a checkable sign certificate.
Available artifacts
arXiv supplies PDF, experimental HTML, and TeX source. No public formal proof, code, data, or numerical certificate repository is linked on the record.
The paper claims a counterexample showing a local-to-global shortcut for certain quadratic forms fails when singular cases are included.
Who did it
Shisong Xu
What it could mean
The local checks can look reassuring while the bigger picture fails. This result would expose that trap for pairs of quadratic forms, showing why a crucial safeguard cannot simply be dropped.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Reconstruct the claimed (K⁷) singular pencil and compute its adjoint closure, hyperbolicity, and weak-hyperbolicity status over a formally real test field; then examination the positive-minimal-index Kronecker-block argument and the dimension-minimality reduction separately.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
For a Pfister-type local--global criterion for nonsingular pairs of quadratic forms, the manuscript claims the nonsingularity hypothesis cannot be removed: over every formally real field it constructs a singular pair on (K⁷) whose adjoint closure is its two-dimensional pencil of hyperbolic forms although the pair is not weakly hyperbolic. The new v2 abstract further claims a complete two-dimensional regular-pencil closure dichotomy and minimality of dimension seven.
Why this could matter
A hidden exception breaks a local-to-global test Local-to-global principles let mathematicians infer an entire object's behavior from easier local checks. This counterexample says one such shortcut for pairs of quadratic forms breaks when singular cases are allowed.
If it holds up
Foundational: mathematicians must retain the nonsingularity safeguard or find a replacement, preventing a false local-to-global rule from propagating through quadratic-form research.
If it does not
First's broader conjecture remains plausible, and the decomposition examination will show which singular-block argument failed.
Impact horizon
Foundational · Quadratic forms · Algebra · Local-to-global methods
Version
revised 2026-08-28 14:03:34 UTC
Why we tracked it
a fresh, substantive v2 expansion of a named-conjecture counterexample, with a bounded algebraic target but no supplied formal or computational replay artifact.
Highest-risk dependency
The universal passage from the explicit example to the stated closure dichotomy depends on the precise treatment of singular Kronecker blocks and the regular part; the abstract alone does not expose the requisite field and decomposition hypotheses.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source; no formal-proof, code, data, or certificate repository is linked on the primary record.
The paper claims an all-level proof of one specified case of the AGT correspondence in mathematical physics.
Who did it
Le-Feng Chen and Kilar Zhang
What it could mean
A four-dimensional physics calculation can have a two-dimensional counterpart. This claim would prove one precise version of that surprising bridge at every expansion level—not collapse the full theory into two dimensions.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Re-derive the factorization and one-box matrix elements; inspect the rational corner-function identity and total-derivative recursion; compare the all-level recurrence with known finite-level calculations under precisely matching genericity assumptions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The authors claim an all-level proof of the four-point SU(2) AGT correspondence with four fundamental hypermultiplets at generic β=-ε₁/ε₂, via generalized-Jack-polynomial Selberg-average factorization and a triangular recursion.
Why this could matter
A major piece of a quantum-physics dictionary may be proved The AGT correspondence links calculations in four-dimensional gauge theory to two-dimensional conformal field theory. This paper claims an all-level proof for the four-point SU(2) case at generic beta—not the entire AGT program.
If it holds up
Foundational: that specific four-point SU(2), generic-beta correspondence becomes a theorem at every expansion level, strengthening one important part of the broader AGT dictionary.
If it does not
Finite-level matches may remain, but the claimed universal translation needs repair—likely in a recursion, factorization, parameter, or normalization step.
Impact horizon
Foundational · Quantum field theory · Mathematical physics · Dualities
It presents itself as a full proof of a named correspondence where the abstract specifies several load-bearing identities and a transition from finite-level evidence to an all-level statement.
Highest-risk dependency
The transition from the stated recursion and factorization identities to the complete AGT correspondence at all levels, including parameter-domain and basis-normalization assumptions.
Available artifacts
No formal-proof, code, or certificate repository was linked on the primary record at retrieval.
The paper claims a sharp control result for functions of matrices up to size three.
Who did it
Per Åhag, Rafał Czyż, Antti Perälä, and Jani Virtanen
What it could mean
Small matrices can hide big numerical surprises. Proving this bound for matrices up to 3×3 could help researchers control errors that an eigenvalue-only view misses.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Per Åhag; Rafał Czyż; Antti Perälä; Jani Virtanen.
See the proposed checks
examination the dimension-three reduction and extremal cases; reproduce finite-dimensional numerical examples independently; compare the complete (matrix-amplified) assertion with the scalar Crouzeix constant and all stated normalization conventions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The manuscript claims to settle the complete Crouzeix conjecture for matrices of order at most three, alongside sharp square-function and spectral-constant results in dimensions two and three.
Why this could matter
Small matrix calculations get a stronger safety bound Functions of non-normal matrices can behave far more wildly than their eigenvalues suggest. This result claims a sharp control principle for matrices up to size three, including matrix-valued calculations.
If it holds up
Enabling: researchers gain firmer error and stability bounds for small-matrix computations, with possible downstream value in numerical analysis, control, and signal processing.
If it does not
The complete Crouzeix bound remains unsettled for 3×3 matrices; a failed proof step would not itself establish a counterexample or a breakdown of scalar intuition.
Impact horizon
Enabling · Matrix stability · Numerical analysis · Operator theory
Version
v1, submitted 2026-08-27 16:46:51 UTC.
Why we tracked it
A resolution claim with a limited dimensional scope gives a comparatively concrete target for independent operator-theory review.
Highest-risk dependency
Whether the square-function estimates establish the complete conjecture under the claimed matrix-amplification norms rather than only the scalar or a restricted-dimensional analogue.
Available artifacts
No formalization, code, or certificate repository was linked on the primary record at retrieval.
A proposed Lean 4 blueprint formalizes norm-variation estimates for interacting processes, with substantial large-language-model assistance.
Who did it
Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, and Christoph Thiele
What it could mean
AI helping with textbook exercises is one thing; AI helping formalize a deep modern theorem is another. Replaying this work would test whether machine assistance can scale while its reasoning stays inspectable.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Floris van Doorn; Polona Durcik; Joris Roos; Lenka Slavíková; Christoph Thiele.
See the proposed checks
Pin a repository commit and run its Lean build in a clean toolchain; identify the formal theorem(s) corresponding to the stated norm-variation result; examination dependency closure, absence of axiomatic escapes, and the prose-to-formal statement map; independently assess the remaining real-variable estimate and hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The blueprint says its Lean 4 formalization, completed largely automatically with frontier large-language-model assistance, supports norm-variation estimates for multiple ergodic averages of commuting transformations, quantitatively strengthening Tao's norm-convergence theorem and answering an Avigad--Rute question.
Why this could matter
A stress test for AI-assisted formal mathematics This mathematics measures whether several interacting processes settle down—and how violently they fluctuate along the way. The bigger story is methodological: a deep modern analysis proof was formalized largely with AI, giving us a rare test of reviewable machine mathematics.
If it holds up
Methods: it would show AI-assisted formalization can carry a large, current analysis theorem into a proof checker, strengthening the case for faster mathematical work whose logical core remains inspectable.
If it does not
A mismatch would expose where the formal theorem, dependencies, or prose diverge—exactly the evidence needed to improve machine-proof workflows before trusting them at scale.
Impact horizon
Methods · AI verification · Dynamical systems · Formal proofs
Version
v1, submitted 2026-08-27 16:21:38 UTC. The linked repository reported an update on 2026-08-29 during retrieval.
Why we tracked it
It is a live, explicitly AI-assisted formalization claim with a stated machine-checkable artifact and a narrow theorem surface suitable for source-to-kernel and source-to-prose scrutiny.
Highest-risk dependency
Whether the repository's kernel-checked statements exactly cover the analytic theorem and claimed quantitative strengthening described in the manuscript, rather than a narrower supporting component.
Available artifacts
arXiv's author comment links the public Lean 4 repository; the paper also links generated documentation and a dependency graph.
A paper claims the full Arnold-Givental lower bound on intersections for a broad class of symmetric geometric systems.
Who did it
Shaoyun Bai, Egor Shelukhin, Yi Wang, and Guangbo Xu
What it could mean
Some shapes cannot be untangled by the motions the mathematics permits. This claimed theorem would make unavoidable intersections predictable in the geometry behind classical mechanics.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Check the integral Floer-theory inputs and their hypotheses; verify the reduction to Hamiltonian Floer cohomology; examine the equivariant-localization construction, transversality requirements, and the passage to the stated mod-2 Betti lower bound.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
For a closed symplectic manifold with an anti-symplectic involution and transverse Hamiltonian image of its fixed locus, the authors claim the Arnold-Givental lower bound on the number of intersection points in full generality.
Why this could matter
A long-standing rule for the geometry of motion Symplectic geometry is the language of systems whose positions and momenta evolve together. This claimed theorem says certain symmetric shapes cannot be moved through phase space without a minimum number of intersections—a deep rigidity rule for the geometry underlying mechanics.
If it holds up
Foundational: it would complete a major rigidity principle in symplectic topology and sharpen the geometric toolkit used to understand Hamiltonian motion, without implying an immediate engineering breakthrough.
If it does not
A failure would locate a gap in the new localization or Floer-theory machinery, preserve only established partial cases, and prevent the full-generality claim from hardening into lore.
Impact horizon
Foundational · Symplectic geometry · Mathematical physics · Dynamical systems
The claim removes the abstract's stated generality restriction and depends on a newly described localization construction in equivariant Floer theory.
Highest-risk dependency
The claimed full-generality extension depends on analytic and orientation/transversality machinery that cannot be inferred from the abstract or a finite calculation.
Available artifacts
No formal-proof, code, or certificate repository was linked on the primary record at retrieval.
A paper claims a standard two-site cell-signaling model can oscillate under rich kinetics but cannot under mass-action kinetics.
Who did it
Nicola Vassena
What it could mean
How do cells find their rhythm? In one signaling model, this result would show how the chosen chemistry rules allow—or block—a specific route to oscillation. It would not rule out every rhythm.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Extract the Routh--Hurwitz reduction, reconstruct the claimed polynomial positivity certificate independently, and separately check the kinetic-model translation; highest risk is whether the certificate covers the complete admissible parameter domain rather than a restricted symbolic regime.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Claims the sequential/distributive dual futile-cycle ODE system permits Hopf bifurcation under parameter-rich kinetics but not under mass-action kinetics; the author explicitly reports a decisive ChatGPT Sol 5.6 contribution to a nontrivial positivity certificate.
Why this could matter
When cell-signaling models can—and cannot—oscillate Cells often control activity by adding and removing chemical tags from proteins. This paper asks when a standard two-site signaling circuit can oscillate, helping researchers avoid attributing rhythmic behavior to a model whose assumptions mathematically forbid it.
If it holds up
Enabling: it would give systems biologists a firmer rule for choosing kinetic models of multisite phosphorylation and a concrete example of AI producing a checkable polynomial certificate.
If it does not
The claimed divide remains unsettled: parameter-rich kinetics may fail to produce the oscillation, mass-action kinetics may fail to exclude it, or both.
Impact horizon
Enabling · Cell signaling · Systems biology · AI-assisted math
Version
submitted 2026-08-27 13:07:36 UTC.
Why we tracked it
fresh AI-assisted mathematical-claim case with a narrowly identifiable positivity-certificate dependency and suitable for a source-to-symbolic examination.
Highest-risk dependency
whether the certificate covers the complete admissible parameter domain rather than a restricted symbolic regime.
Available artifacts
No new usable Slack packet or SocialBot signal. Attention evidence is the fresh primary submission and explicit author disclosure on the primary abstract page. arXiv provides PDF, experimental HTML, and TeX source; no separate formal-proof or code artifact is linked.
A paper claims exact formulas for the largest number of queens that can be placed when each attacks at most one other.
Who did it
Kristina Ago, Bojan Bašić, and Radojka Ciganović
What it could mean
How crowded can a chessboard get before its queens fight too much? This claim would give an exact answer for every board size when each queen may attack at most one other.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Independently verify the constructions by residue class and derive the matching upper bound from the attack-graph constraints; highest risk is a hidden exceptional-board or boundary case in the upper-bound reduction.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
States (q(n)=lfloor4n/3rfloor) for every (nge6), and (q(n)=n) for (nle5), where every placed queen attacks at most one other; it also gives the stated exact-one-attacker formula. This is a new primary-source claim to settle previously conjectural values.
Why this could matter
A chessboard puzzle gets an exact answer This gives an exact answer to a deceptively hard chessboard question: how many queens fit when each may attack at most one other? Beyond the puzzle, it is a clean case study in turning clever constructions into universal upper bounds.
If it holds up
Foundational: it closes the puzzle for every board size and supplies compact constructions and bounds that can benchmark human or machine combinatorial reasoning.
If it does not
A missed board size or boundary case would reveal where the proposed universal formula needs an exception or a stronger upper-bound argument.
Impact horizon
Foundational · Recreational math · Combinatorics · Optimization
Version
submitted 2026-08-27 17:53:25 UTC.
Why we tracked it
fresh, exactly stated resolution of a finite extremal-combinatorics problem; compact enough for a bounded independent construction and upper-bound examination.
Highest-risk dependency
a hidden exceptional-board or boundary case in the upper-bound reduction.
Available artifacts
No new usable Slack packet or SocialBot signal. Attention evidence is the fresh primary submission. arXiv supplies PDF, experimental HTML, and TeX source; no formal-proof, code, or certificate repository is linked on the record.
A paper claims a finite counterexample to the Non-Cancelling-Intersections conjecture about set operations and inclusion-exclusion.
Who did it
Hermann Wilhelm
What it could mean
The numbers can add up perfectly while the promised construction is impossible. This counterexample would break a proposed bridge between tidy counting formulas and the actual sets they describe.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Source-lock the original NCI statement and 2608.19414, then reconstruct the marked-plane admissibility gap and the plane-tree-to-dot-algebra implication; highest risk is that the new tree-shaped argument does not eliminate every non-left-linear representation.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Claims a finite lattice whose top element has no dot-algebra representation, removing the left-linearity restriction from the author's earlier 2608.19414 result and thereby refuting the NCI conjecture as stated.
Why this could matter
Some clean formulas have no clean construction The conjecture promised that whenever inclusion–exclusion computes a union without algebraic cancellation, the same result could be built from literal set operations. A counterexample means some tidy numerical identities have no equally tidy structural explanation.
If it holds up
Foundational: it would block a tempting shortcut in symbolic set reasoning: not every cancellation-free numerical identity can be converted into an equally transparent construction.
If it does not
The original structural hope survives, and the finite lattice construction reveals which representation step still needs repair.
Impact horizon
Foundational · Combinatorics · Set systems · Symbolic reasoning
Version
submitted 2026-08-27 17:42:42 UTC.
Why we tracked it
fresh explicit claimed counterexample to a named conjecture, with a finite combinatorial witness route but a dependency on a prior restricted-case paper.
Highest-risk dependency
that the new tree-shaped argument does not eliminate every non-left-linear representation.
Available artifacts
No new usable Slack packet or SocialBot signal. Attention evidence is the fresh primary submission. arXiv provides PDF, experimental HTML, and TeX source; no formal/code artifact is listed.
A paper claims an exact density threshold forcing many consecutive even loop sizes in sufficiently large networks.
Who did it
Yaobin Chen, Hong Liu, Xia Wang, Xin Wei, and Fan Yang
What it could mean
Pack enough connections into a network and whole runs of even-sized loops become unavoidable. This theorem would identify the exact threshold for that hidden order in the stated large-size regime.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Yaobin Chen; Hong Liu; Xia Wang; Xin Wei; Fan Yang.
See the proposed checks
Pin the exact quantifier behind “sufficiently large,” then examination the dense-core decomposition and rooted-cycle-family coverage against the equality case; highest risk is a gap in recovering all required consecutive lengths after the expander extraction.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
For sufficiently large (t), claims the sharp Erdős--Gallai edge threshold forces (t) consecutive even cycle lengths, resolving a conjecture of Verstraëte and deriving stated residue-class cycle-threshold consequences.
Why this could matter
Dense networks must hide loops of many sizes In a dense network, loops are unavoidable. This theorem claims something much sharper: once a graph crosses an exact density threshold, it must contain loops of many consecutive even sizes, revealing a surprisingly rigid law of network structure.
If it holds up
Foundational: it would give graph theorists a sharp guarantee about the cycle lengths hidden inside dense networks, strengthening the structural toolkit behind extremal graph algorithms.
If it does not
The proposed threshold or exceptional case is incomplete, warning researchers not to use it as a universal guarantee about dense graphs.
Impact horizon
Foundational · Graph theory · Network structure · Combinatorics
Version
submitted 2026-08-27 17:32:57 UTC.
Why we tracked it
fresh resolution claim for a named extremal-graph conjecture, with clear scope and a potentially decomposable proof examination.
Highest-risk dependency
a gap in recovering all required consecutive lengths after the expander extraction.
Available artifacts
No new usable Slack packet or SocialBot signal. Attention evidence is the fresh primary submission. arXiv provides PDF, experimental HTML, and TeX source; no public formalization or code/certificate link appears on the record.
The authors propose similarity rules that work in flat space but fail on spheres in every even dimension.
Who did it
Wentao Huang and Haizhang Zhang
What it could mean
The Earth is round; a statistical model cannot always pretend otherwise. These examples would show how valid flat-space similarity rules can fail on spheres—a warning for geographic data and machine learning.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Verify even/odd dimensional scope, exact support, and both positive-definiteness assertions; highest risk is the function-class and distance-kernel correspondence.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
For each even dimension and admissible support radius, constructs a smooth radial kernel that is strictly positive definite in Euclidean space but not positive definite on the sphere.
Why this could matter
Flat-space models can break on a round world Positive-definite kernels are the similarity and covariance rules behind spatial statistics and many machine-learning methods. This result warns that a kernel valid on flat space can become mathematically invalid on a sphere—crucial for Earth-scale and directional data.
If it holds up
Enabling: modelers gain exact examples showing when flat-space kernels can produce impossible covariance structures on spherical data, supporting safer geometry-aware choices in geospatial statistics and machine learning.
If it does not
The claimed even-dimensional failure narrows or disappears, so some flat-space kernels may transfer more safely than the construction suggests.
Impact horizon
Enabling · Spatial statistics · Kernel methods · Spherical data
Version
submitted 2026-08-26 11:07:13 UTC.
Why we tracked it
a specific refinement of an already known transfer failure, rather than a newly named-conjecture resolution.
Highest-risk dependency
the function-class and distance-kernel correspondence.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
A Lean 4 formalization claims to exclude a bounded class of repeating odd-period schedules that cover every integer.
Who did it
Ibrahim Mian and Shayaan Siddique
What it could mean
A computer search can say ‘nothing works.’ This work aims to turn that verdict into a replayable proof: no qualifying odd-period cover with combined period at most 10,000—not the whole conjecture.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Clean pinned Lean replay, axiom closure, source-to-Lean statement correspondence, and verification of the finite Chinese-remainder certificates; highest risk is scope correspondence, especially that the formal statement matches the intended covering-system exclusion.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Lean 4 kernel formalization of the finite exclusion (operatornamelcm>10000) for odd distinct-modulus covers, with 63 public theorems and stated no-sorry/no-nativedecide trust boundary.
Why this could matter
A giant number search becomes checkable proof Imagine covering every integer with repeating schedules that use distinct odd periods. The grand puzzle remains open, but this work machine-checks that no such system can have a combined period of 10,000 or less—a milestone for reviewable computational proof.
If it holds up
Methods: it demonstrates one reproducible route from search-generated certificates to Lean-kernel theorems for this bounded exclusion; broader reuse needs separate evidence.
If it does not
A scope or trust-base mismatch would show why compiled code is not enough and protect later searches from inheriting a false foundation.
Impact horizon
Methods · Formal proof · Number theory · Verified computation
Version
submitted 2026-07-28 12:10:26 UTC.
Why we tracked it
a high-value formal-proof artifact, though the authors state that its mathematical exclusion is known and its advance is epistemic/formal.
Highest-risk dependency
scope correspondence, especially that the formal statement matches the intended covering-system exclusion.
Available artifacts
The paper links Lean sources, certificates, and CI on GitHub; no current social signal used.
The authors introduce a 13-domain benchmark for testing whether theorem-proving systems reason, formalize, and survive harmless rewording.
Who did it
Jiaxin Yuan and colleagues
What it could mean
Change the wording, keep the math. Does the AI still succeed? This benchmark could expose the gap between genuine mathematical reliability and a system that only looks brilliant on familiar questions.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Re-run the Lean verifier against a clean Mathlib workspace; sample transformed-problem equivalences; inspect whether reported completion criteria exclude remaining sorry; reproduce a bounded subset of the published benchmark runs.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The authors introduce a 13-domain diagnostic benchmark for natural-language and Lean 4 theorem proving, including reformulation tests, and report that formalization remains a bottleneck and equivalent restatements expose robustness limits.
Why this could matter
Can math AI survive a simple rewording? Can an AI prove the same theorem when the wording changes? This benchmark tests theorem provers across 13 areas and finds that many stumble on formalization or equivalent restatements, exposing the difference between genuine robustness and a flattering headline score.
If it holds up
Methods: it gives developers a better diagnostic map for building math assistants that generalize across subjects and survive harmless rewording, rather than merely excelling on familiar benchmark formats.
If it does not
If transformed problems are not truly equivalent or scoring is leaky, model rankings could mislead research; fixing the benchmark still improves evaluation.
Impact horizon
Methods · AI evaluation · Theorem proving · Benchmarks
Version
v1, submitted 2026-08-26 07:12:54 UTC.
Why we tracked it
Its released JSONL data, Lean verification utility, runners, and preserved result structure offer a concrete reproducibility target for evaluating the distinction between compilation, completion, and semantic interpretation.
Highest-risk dependency
Whether each informal/reformulated prompt preserves the intended formal statement and whether benchmark scoring separates kernel acceptance from semantic faithfulness.
Available artifacts
The repository provides benchmark JSONL, Lean 4 verification through lake exe repl, task runners, and the released junk-theorem study artifacts.
A paper claims a counterexample to a century-old expectation about how complex functions behave in a half-plane.
Who did it
Yixin He and Teng Zhang
What it could mean
Three reassuring clues may tell you surprisingly little about a function’s hidden behavior. This claimed counterexample would overturn a century-old expectation about controlling complex functions—forcing the rules to be rewritten.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Reconstruct the stated meromorphic function from the TeX source; independently verify the three-value preimage condition and the failure of bounded type in the upper half-plane; obtain specialist review of the Nevanlinna-class criterion used.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
The authors construct a nonconstant meromorphic function on the complex plane whose preimages of 0, 1, and infinity lie on the real axis, while its restriction to the upper half-plane is not in the Nevanlinna class; this is presented as a counterexample to Nevanlinna's half-plane problem.
Why this could matter
A century-old shortcut in complex analysis may fail A century-old expectation said that a complex function avoiding three values in half a plane must behave in a controlled way there. This construction says no, forcing analysts to rethink which geometric clues actually guarantee tame growth.
If it holds up
Foundational: it removes a trusted shortcut in complex analysis and launches the search for stronger conditions that really control meromorphic functions in a half-plane.
If it does not
The century-old principle survives; the construction would teach precisely where its claimed preimage or growth property breaks.
Impact horizon
Foundational · Complex analysis · Function theory · Mathematical foundations
Version
v1, submitted 2026-08-25 17:10:32 UTC; 13 pages.
Why we tracked it
A newly posted claimed counterexample to a long-standing complex-analysis question is compact enough for a source-lock and construction-level examination.
Highest-risk dependency
Whether the construction simultaneously establishes the global preimage condition and the claimed non-membership in (N(H)), including any growth or boundary argument.
A paper claims predicted polynomial-constraint counts for two specific equation degrees in four variables, while leaving the broader conjecture open.
Who did it
Dongming Zhang and Qihang Wang
What it could mean
Computer algebra needs to know how many constraints really remain in a tangle of equations. These certificates would settle two difficult cases—degrees five and seven in four variables—not the whole conjecture.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Run the supplied verifiers from a locked source bundle; independently reimplement modular maximal-minor/rank checks and compare certificate hashes; check the Zariski-openness transfer and endpoint reductions against the exact stated ranges.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
For equal-degree ideals in four variables over characteristic-zero fields, the paper establishes Fröberg's predicted Hilbert series for every generator count when the degree is 5 or 7, using finite Macaulay-multiplication rank certificates; it expressly leaves the unrestricted conjecture outside scope.
Why this could matter
Two hard families of polynomial systems become predictable Hilbert series tell algebraists—and computer-algebra software—how many independent polynomial constraints remain at each degree. This paper settles two difficult degree cases, making generic systems of quintic and septic equations more predictable, while leaving the full conjecture open.
If it holds up
Enabling: the exact rank certificates could give computer-algebra researchers reliable formulas and reproducible test cases for generic polynomial ideals in these two degrees.
If it does not
A failed certificate or reduction would limit the covered generator ranges and prevent algebra systems from relying on an overstated formula.
Impact horizon
Enabling · Computer algebra · Polynomial systems · Verified computation
The result has a specific new scope and ships Python verifiers plus a JSON certificate, making an independent exact replay materially more immediate than for a prose-only claim.
Highest-risk dependency
The correctness and completeness of the endpoint-to-all-(r) reduction, and whether the modular nonzero-minor certificates cover every claimed new generator-count slice.
Available artifacts
arXiv ancillary files frobergquinticsverifier.py, frobergsepticscertificate.json, and frobergsepticsverifier.py are linked on the primary record.
A paper claims a translation rule between topological and algebraic records of singularities in plane curves.
Who did it
Sheng Tan
What it could mean
A curve can cross or pinch itself in complicated ways. This theorem would let mathematicians translate clues between geometry and algebra—making the same difficult singularity readable in more than one language.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Map the exact plane-curve theorem and test the iterated-residue obstruction; highest risk is scope between maximal-order/general poles and the plane-curve conclusion.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Claims the topological multivariable Strong Monodromy Conjecture for reduced plane-curve germs, via containment of actual polar hyperplanes in the Bernstein–Sato zero locus.
Why this could matter
Two languages for mathematical singularities may finally agree When an algebraic curve crosses or pinches itself, topology and algebra record the damage differently. This theorem claims that, for plane curves, a signal seen in one record must appear in the other—a powerful translation rule for singularities.
If it holds up
Foundational: it would strengthen the dictionary between geometric, topological, and algebraic descriptions of curve singularities, helping researchers compute and classify these complicated points from whichever representation is tractable.
If it does not
The full plane-curve theorem remains unproved; a failed step may reveal a gap or missing hypothesis, but would not by itself show that counterexamples exist.
Impact horizon
Foundational · Singularity theory · Algebraic geometry · Topology
Version
submitted 2026-08-26 17:50:51 UTC.
Why we tracked it
a fresh plane-curve scope claim with a stated route through Bernstein–Sato and zeta loci.
Highest-risk dependency
scope between maximal-order/general poles and the plane-curve conclusion.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
The first of two papers proposes a proof of the Generalised Cone Conjecture for surfaces beyond Calabi-Yau cases.
Who did it
Vladimir Lazić, Isabel Stenger, and Zhixin Xie
What it could mean
An infinity of geometric possibilities could fit into a finite-sided map. If this paper and its companion hold, symmetry would make a daunting family of surfaces far more manageable.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
The authors state that this first paper proves the Generalised Cone Conjecture on surfaces.
Why this could matter
Turning infinite geometric complexity into a finite map Algebraic surfaces can carry infinitely complicated families of geometric configurations. The cone conjecture says symmetry may compress that infinity into a finite-sided fundamental region, making classification manageable; this paper supplies only part of a two-paper proof.
If it holds up
Foundational: together with its companion, it would organize broad classes of surfaces into finitely describable symmetry regions and support finiteness results for their minimal geometric models.
If it does not
Because this installment treats a companion theorem as a black box, failure there would block the advertised full result while leaving this paper's intermediate theorems potentially intact.
A paper claims a complex-function counterexample that challenges whether three special values control half-plane behavior; authors report machine-generated core work.
Who did it
Quanyu Tang, Bokai Cui, Wei He, Tao Hu, Yanyang Li, Ke Wang, and Zijun Yu
What it could mean
An AI-generated argument may have found a hole in a century-old mathematical expectation. Verifying it would both sharpen the rules for complex functions and put a concrete machine-discovery claim to the test.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Quanyu Tang; Bokai Cui; Wei He; Tao Hu; Yanyang Li; Ke Wang; Zijun Yu.
See the proposed checks
Independently reconstruct the function and prove the half-plane growth/divisor assertions; highest risk is the global analytic passage from the construction to the bounded-type and Blaschke conclusions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Constructs a real meromorphic function with the three designated preimage sets real, not of bounded type in either half-plane, and stronger non-Blaschke statements; the authors say the core construction/proof was generated during an autonomous GPT-5.6 Sol Ultra run.
Why this could matter
A century-old shortcut may finally be broken The claim says three special output values do not control a complex function's behavior in a half-plane as mathematicians had hoped. Because the core argument was machine-generated, it is also a striking test of autonomous mathematical discovery.
If it holds up
Foundational: complex analysts lose a century-old shortcut and gain a new example that redraws the boundary between special-value data and global growth.
If it does not
The old question stays open, while the failed construction shows exactly where autonomous reasoning lost control of an infinite analytic argument.
fresh claimed century-scale counterexample with an explicit AI-generated core construction; compare before any docket action with the related Nevanlinna intake below.
Highest-risk dependency
the global analytic passage from the construction to the bounded-type and Blaschke conclusions.
Available artifacts
Fresh primary submission; no formal or code artifact linked on the arXiv record; no current social signal used.
A paper claims groups with unusually economical generation but arbitrarily large hidden topological complexity, contradicting a 2011 conjecture.
Who did it
Sam P. Fisher and Yash Lodha
What it could mean
An economical algebraic description can hide unlimited topological complexity. This claimed counterexample would break a proposed shortcut for judging how complicated a mathematical structure really is.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Check the construction's torsion-free/local-free/normal-rank properties and the (ℓ²)-Betti calculation; the load-bearing ambiguity is whether all properties coexist in the stated countable, non-finitely-generated group.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
For each (n), constructs a countable torsion-free locally free group with first (ℓ²)-Betti number (n) and normal rank one, contradicting the 2011 Osin--Thom conjecture.
Why this could matter
One generator may hide unlimited topological complexity A group can be generated in an unexpectedly economical way yet carry arbitrarily large hidden topological complexity. That breaks a proposed bridge used to reason about several major open problems in group theory and topology.
If it holds up
Foundational: researchers must uncouple normal generation from this complexity measure and revisit consequences tied to the Wiegold, Levin, Kervaire, and Whitehead problems.
If it does not
The conjectured bridge survives, and the construction reveals which finiteness or generation condition is doing the real work.
Impact horizon
Foundational · Group theory · Topology · Mathematical foundations
Version
submitted 2026-08-26 16:38:37 UTC.
Why we tracked it
fresh, compact claimed disproof with a clearly stated construction, but no public formal/computational artifact.
Highest-risk dependency
The claim has not been independently examined beyond source locking.
Available artifacts
Fresh primary submission; no formal/code artifact linked; no current social signal used.
A paper claims a counterexample showing that continuously changing compatible information need not combine into one global mathematical model.
Who did it
Morgan Rogers and Joshua Wrigley
What it could mean
All the local pieces can look compatible without a whole ever existing. This counterexample would expose that trap in mathematical model-building: continuous local information is not automatically a global solution.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Map coherence, continuity, fibre realization, and sheaf-model notions to the original problem; highest risk is a mismatch between the construction and Kanalas' hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Gives a coherent theory, space, and continuous type assignment for which no corresponding sheaf model realizes the assigned types fibrewise, negatively answering a problem of Kristóf Kanalas.
Why this could matter
Smooth local choices can still refuse to assemble The paper tests a powerful mathematical instinct: if compatible information changes continuously from place to place, it should combine into one coherent global model. This counterexample says continuity alone is not enough.
If it holds up
Foundational: theories that build global objects from local data need stronger compatibility conditions, sharpening the logic behind sheaves and local-to-global reasoning.
If it does not
A promising local-to-global principle remains alive, and the attempted counterexample exposes which hypothesis actually guarantees assembly.
Impact horizon
Foundational · Logic · Category theory · Local-to-global models
Version
submitted 2026-08-26 12:08:01 UTC.
Why we tracked it
a compact negative answer with a claim-mappable construction.
Highest-risk dependency
a mismatch between the construction and Kanalas' hypotheses.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
A paper claims to complete a conjecture linking practical numbers with a broad family of quadratic formulas.
Who did it
Ting Hon Stanford Li
What it could mean
Imagine numbers whose divisors act like coins, each used once, that can make every smaller amount. This result, combined with earlier work, would complete a promised connection between those numbers and quadratic formulas.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Extract both original Wang–Sun parts, verify the practical-number conclusion and the dependency on Somu–Li–Kukla; highest risk is that the combined-result claim exceeds the paper's self-contained proof.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Proves the second Wang–Sun component for odd b and even c; with earlier named work, the author says this settles the full conjecture.
Why this could matter
Quadratic recipes keep finding unusually flexible numbers Practical numbers can make every smaller amount from distinct divisor “coins.” This result would finish a conjecture showing that a broad family of quadratic formulas is guaranteed to produce one of these unusually flexible numbers.
If it holds up
Foundational: it closes the Wang–Sun conjecture and gives number theorists a dependable recipe connecting quadratic expressions with divisor-sum structure.
If it does not
The full conjecture remains open, and the failure identifies whether the new proof or its reliance on earlier work needs repair.
Impact horizon
Foundational · Number theory · Divisor structure
Version
submitted 2026-08-26 10:04:03 UTC.
Why we tracked it
an explicitly scoped final component of a named number-theory conjecture.
Highest-risk dependency
that the combined-result claim exceeds the paper's self-contained proof.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
The authors propose curved spaces whose boundary vibration frequency falls below a proposed limit despite favorable curvature and shape conditions.
Who did it
Fagui Li and Yuhang Zhao
What it could mean
A nicely curved shape can still break an expected rule about boundary vibrations. This counterexample would show why attractive geometric safeguards alone cannot guarantee the frequency floor mathematicians predicted.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
examination the conformal deformation, strict inequalities, and eigenvalue perturbation; highest risk is whether the proposed strengthening and its function-space hypotheses are precisely those refuted.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Constructs hemisphere metrics with strict Ricci and boundary-convexity inequalities but first boundary Laplace eigenvalue below the proposed bound in every dimension at least three.
Why this could matter
Curved spaces can vibrate below the expected floor Eigenvalues encode natural vibration and wave frequencies. The paper says even positively curved spaces with nicely convex boundaries can fall below a proposed frequency floor, showing that those geometric safeguards are not enough.
If it holds up
Enabling: spectral and geometric models gain a sharper warning about which shape and curvature assumptions can safely predict boundary-wave behavior.
If it does not
The proposed spectral floor may survive, and the deformation pinpoints where curvature or boundary conditions prevent the claimed exception.
A paper claims an explicit deformation of a three-dimensional ball that violates a proposed boundary-vibration lower bound.
Who did it
Alexandre Girouard and Thomas Hélière
What it could mean
Even a distorted ball can overturn a long-standing geometric prediction. This explicit example would show why positive curvature and a convex boundary cannot guarantee the lowest boundary-response frequency mathematicians expected.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Reconstruct the metric, curvature and boundary-convexity calculations, then the Steklov comparison; highest risk is simultaneous satisfaction of the geometric hypotheses in the conjecture's exact regime.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
An explicit polynomial deformation of the unit three-ball has positive Ricci curvature and strictly convex boundary while violating Escobar's proposed first nonzero Steklov-eigenvalue lower bound.
Why this could matter
A nearly round ball challenges a spectral-geometry prediction Steklov eigenvalues measure how harmonic behavior inside a shape responds at its boundary. This explicit deformation of a three-dimensional ball appears to violate a curvature-and-boundary prediction, offering a sharp mathematical benchmark rather than a general wave-engineering result.
If it holds up
Foundational: spectral geometers gain a concrete counterexample showing that positive curvature and convexity do not guarantee the proposed Steklov bound.
If it does not
Escobar's proposed bound survives this attack, and the calculation exposes which geometric condition the candidate shape fails to satisfy.
A paper claims to settle a bounded-height case of Frankl's union-closed-sets conjecture and constrain the next cases.
Who did it
Chenxiao Tian
What it could mean
Merge any two sets and get another allowed set. Must some item appear in half of them? This claim would settle a bounded class of that puzzle—not the general answer.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Map the two formulations and reproduce the height-four case analysis; highest risk is a formulation/height shift being read as a result beyond the exact stated scope.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Proves the union-closed-sets conjecture for empty-set-free families of height at most four (equivalently usual families containing the empty set of height at most five), and constrains possible height-five counterexamples.
Why this could matter
A stubborn set puzzle loses another escape route The puzzle asks whether some item must appear in at least half the sets whenever combining any two stays inside the family. This paper settles height four and constrains the smallest height-five counterexamples; taller cases remain open.
If it holds up
Foundational: it settles height four and narrows the smallest height-five counterexamples, guiding the next search without resolving Frankl's conjecture in full.
If it does not
The height-four frontier reopens, but the broken step reveals which structural constraint cannot be trusted in future attacks.
Impact horizon
Foundational · Combinatorics · Set systems · Extremal structures
Version
submitted 2026-08-25 20:55:41 UTC.
Why we tracked it
a sharply limited new theorem plus structural constraints, not a full resolution.
Highest-risk dependency
a formulation/height shift being read as a result beyond the exact stated scope.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
A paper claims that failures of a uniform number-approximation rule form a large fractal family, not isolated exceptions.
Who did it
Nikita Shulga
What it could mean
The failures are not isolated glitches; they form a substantial fractal landscape. This result would measure how extensively a uniform number-approximation rule breaks down, without resolving the classical Littlewood conjecture.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Pin the exact ULC quantifiers, verify the dimension argument, and trace dependence on Schleischitz's earlier counterexample result; highest risk is conflation with classical Littlewood.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Establishes a Hausdorff-dimension-at-least-3/2 counterexample set in a badly-approximable slice and a full-dimension projection statement for the uniform—not classical—Littlewood conjecture.
Why this could matter
Number-pair exceptions may form a surprisingly large fractal A uniform number-approximation rule was already known to fail. This paper says the failures occupy a genuinely large fractal family, changing them from isolated oddities into a substantial part of the mathematical landscape.
If it holds up
Foundational: researchers gain a quantitative map of where uniform simultaneous approximation fails, with new tools for measuring exceptional fractal sets.
If it does not
The known counterexamples remain, but claims that they form a large fractal family must be scaled back.
Impact horizon
Foundational · Diophantine approximation · Fractal geometry · Number theory
Version
submitted 2026-08-25 18:54:02 UTC.
Why we tracked it
a fresh quantitative refinement of a recently claimed ULC failure, with a concrete dimension assertion.
Highest-risk dependency
conflation with classical Littlewood.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
A paper claims that counterexamples to a uniform number-approximation conjecture form a robust, full-dimensional fractal set.
Who did it
Chengyang Wu and Bohan Yang
What it could mean
A handful of exceptions? More like a whole fractal landscape. This result would show a previously proposed family of uniform-approximation counterexamples has the plane’s full fractal dimension—not just scattered failures.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Source-lock BFK25 and map its counterexample set to the displayed limsup; highest risk is treating a property of an asserted set as an independent first counterexample.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Shows the BFK25-proposed ULC counterexample set is hyperplane absolute winning, hence full Hausdorff dimension in (ℝ²).
Why this could matter
These mathematical exceptions may be remarkably hard to erase The authors claim these counterexamples are not just numerous: they form a robust, full-dimensional fractal set and remain large on broad families of curves and lines. That makes the conjecture's failure structurally durable, not accidental.
If it holds up
Foundational: the exceptional set becomes robust enough to study with powerful game-based tools, reshaping the geometry of uniform approximation.
If it does not
The earlier counterexamples may still stand, but their claimed robustness and full-dimensional structure would remain unproved.
Impact horizon
Foundational · Diophantine approximation · Fractal geometry · Mathematical games
Version
submitted 2026-08-25 11:04:24 UTC.
Why we tracked it
a consequential property of a previously proposed counterexample set, best reviewed alongside 2608.25059.
Highest-risk dependency
treating a property of an asserted set as an independent first counterexample.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
A paper reports a 64-node network with no short loops that still needs four colors, supported by SAT and Lean certificates.
Who did it
Glauco Rampone
What it could mean
Even a network without short loops can demand four colors. This 64-node construction would tighten the known size range—and show how computer searches can leave evidence others can replay.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Re-run the witness and SAT/Lean checks from locked sources; separately examination the exhaustive lower-bound computation; highest risk is completeness of the search/certificate bridge for the lower bound.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Improves the known range to (29 ≤ n₆(4) ≤ 64), supplies an explicit 64-vertex witness, and reports a Lean-checked non-3-colourability certificate.
Why this could matter
A smaller impossible-to-three-color network has been found The paper finds a 64-node network with no short loops that still needs four colors, then uses SAT and Lean certificates to check it. It advances both an extremal graph puzzle and reviewable computer-assisted mathematics.
If it holds up
Methods: it tightens the known size range and demonstrates how search, independent code, certificates, and formal proof can support one verifiable result.
If it does not
The failure would expose whether the graph witness, exhaustive search, SAT certificate, or formal checker broke—valuable evidence for better verification pipelines.
Impact horizon
Methods · Graph theory · Formal verification · SAT solving
Version
submitted 2026-08-24 11:14:46 UTC.
Why we tracked it
a narrowly stated extremal result with independent scripts, SAT certificates, and a linked Lean 4 formalization.
Highest-risk dependency
completeness of the search/certificate bridge for the lower bound.
Available artifacts
New Slack discovery packet; G64 repository, independent scripts, SAT certificates, and Lean 4 proof are linked by the primary record.
A computer-assisted paper claims a bounded Hodge-conjecture result for odd-degree Fermat fourfolds through degree 199.
Who did it
Rifat Jumagulov
What it could mean
A foothold in one of mathematics’ biggest mysteries could become computer-checkable: hidden features of four-dimensional shapes. This claim covers a specific Fermat family through degree 199—not the full Hodge conjecture.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Fresh clean-environment replay of the census, certificate hashes, independent enumeration, and prose-to-code/Lean correspondence; highest risk is completeness of the orbit classification and the geometric validity of each closure criterion.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
A computer-assisted proof for odd-degree Fermat fourfolds through degree 199, combining geometric closure criteria with an exhaustive ((2,2))-orbit census.
Why this could matter
A machine-checkable foothold on a million-dollar mystery The Hodge conjecture asks whether certain hidden geometric features always come from actual algebraic shapes. This paper does not solve it generally, but claims a fully checkable proof for a large, precisely bounded family of four-dimensional Fermat varieties.
If it holds up
Methods: it provides a demanding, replayable case study combining geometry, exhaustive computation, independent enumeration, certificates, and Lean on one bounded family.
If it does not
The general conjecture is untouched; the replay would reveal whether the census, geometric closure rules, or code-to-proof bridge failed.
source-locked, narrow finite scope, and unusually rich independent replay surface; no docket created.
Highest-risk dependency
completeness of the orbit classification and the geometric validity of each closure criterion.
Available artifacts
Primary record links ancillary code, data, SHA-256 inventory, certificates, a smoke tier, and a GitHub Lean formalization; no current social signal used.
A computer-assisted paper claims a noncircular flat shape can pass tests once thought to force a disk.
Who did it
Matthew J. Colbrook and George Stepaniants
What it could mean
Can measurements fool you about a shape? This claimed noncircular example would pass tests once thought to single out a disk—exposing a blind spot in what those measurements can tell us.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Reproduce the listed polynomial, interval for (k), linearisation positivity, tail bounds, and contraction certificate; highest risk is the numerical-to-exact bridge that establishes a genuine analytic domain and boundary conditions.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Constructs a bounded simply connected noncircular planar domain yielding counterexamples to the stated Schiffer and Pompeiu formulations through a cubic operator equation and rigorous tail control.
Why this could matter
A strange shape may fool two classic tests Some mathematical tests were thought to force a flat shape to be a disk. This paper constructs a noncircular region that appears to pass the same boundary and integral tests, changing what measurements can reveal about shape.
If it holds up
Enabling: inverse-problem and wave researchers gain a concrete warning that these measurements do not uniquely identify circular geometry, plus an exact benchmark for future methods.
If it does not
The conjectures survive, and the failed numerical-to-exact step identifies where an approximate shape stopped being a genuine mathematical counterexample.
A paper claims an all-dimensional lower bound for allowed wave patterns in round spaces with reflecting boundaries.
Who did it
Yutian Li
What it could mean
How many wave patterns fit below a given frequency? This result would guarantee a minimum for Euclidean balls in every dimension—a sharper benchmark for tackling more complicated shapes.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Replay the supplied certificates independently, then examination the bridge from Bessel/Robin estimates and finite layers to the all-dimensions statement; the load-bearing risk is that analytic uniformity exceeds what the finite checks establish.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Establishes the Neumann Pólya lower bound for Euclidean balls in every dimension, with exact-rational ancillary verification for a two-parameter estimate in dimensions at least seven.
Why this could matter
Round spaces get a guaranteed minimum of wave modes Neumann eigenvalues describe allowed wave patterns in spaces with reflecting boundaries. This paper claims a sharp lower bound—not an exact mode count—for Euclidean balls in every dimension, giving spectral geometry a rigorous benchmark without promising an immediate device.
If it holds up
Enabling: researchers gain an all-dimensional lower-bound benchmark for wave-mode counts in round domains and a stronger base for estimates on harder shapes.
If it does not
The expected lower bound remains unproved for Euclidean balls, so this proposed all-dimensional benchmark cannot yet be treated as established.
Impact horizon
Enabling · Spectral theory · Acoustics · Wave physics
substantive v3 revision in the sweep window and multiple supplied exact/replayable certificate routes.
Highest-risk dependency
The claim has not been independently examined beyond source locking.
Available artifacts
Primary record links certificate manifest, generated outputs, independent Wolfram replay scripts, and verifier programs; no current social signal used.
Current boundary
Intake record only; examination not started.
This is a bounded, high-signal discovery list—not a complete feed of new mathematics. Mathematical findings appear only in full proof dockets.
