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. Evidence differs across theoretical results, experiments, research methods and capability benchmarks. Independent examination is not started unless a separate scoped record says otherwise.
Browse disciplines: Mathematics (89) · Physics (6) · Biology (4). Counts overlap for cross-disciplinary work; tracked entries are not a count of new proofs.
A manuscript claims an algorithm that counts solutions to fixed-width Boolean formulas in subexponential time and polynomial space.
Who did it
OpenAI; an external group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams will examine and explain the work.
What it could mean
If correct, it would overturn a widely used assumption about worst-case computing time. It does not resolve P versus NP or demonstrate a practical solver improvement.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Inspect the fixed-k quantifiers, canonical encoding and concrete machine endpoint, then compare its time and all-prefix space bounds with the manuscript. Keep the manuscript's single-log-log factor and sparse-clause refinement separate from Lean's squared-log-log factor. Select one bounded correspondence check before any isolated replay; no P=NP or practical speedup follows.
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 branching tiles introduce the combinations in a Boolean search. The gathered ribbons are a conceptual metaphor, not the submitted algorithm or a measured speedup.
For fixed k≥2, the manuscript claims exact counting on n-variable, m-clause k-CNF formulas in (n+m)^Ok(1) times 2^Ok(n log log n / sqrt(log n)), using polynomial space; for m≤Dn with fixed D, the exponent improves to O(k,D)(n / sqrt(log n)). The public Lean scope instead gives the weaker exponent Ok(n (log log n)² / sqrt(log n)) with a polynomial canonical-input-length factor, still subexponential.
Why this could matter
A central assumption about computing time faces a claimed refutation Many conditional speed limits assume that solving three-variable Boolean clauses needs exponentially growing time. The claimed algorithm grows more slowly asymptotically and also counts solutions. The public formalization advertises a weaker time bound than the manuscript.
If it holds up
Researchers would revisit hardness claims that depend on ETH and investigate which algorithmic ideas yield useful improvements on actual workloads.
If it does not
A failed reduction, time bound or formal correspondence would identify the gap; it would not prove ETH true.
2026-10-25; October 17 manuscript, revised October 25, 2026; public release at Git commit 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a.
Why we tracked it
source-reviewed intake only; independent examination has not started.
Highest-risk dependency
Analyst judgment: the precise fixed-width encoding, machine-cost model, reduction overhead and manuscript-to-Lean correspondence are load-bearing. Lean's advertised exponent has (log log n)²; the sharper prose bound has log log n, with an additional sparse-case improvement. A replay of the weaker endpoint would not by itself certify those sharper bounds. This is source intake only, not proof validation, polynomial-time SAT or demonstrated commercial acceleration.
Available artifacts
Pinned openai/math 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a; paper.pdf (Git blob 0503566e95bc587a4076573a45132d97531b8ba6), lean/docs/378.md, lean/OAI/Algorithms/SubexponentialSAT/SqrtLogSpace/Final.lean and lean/ComparatorChallenges/SubexponentialSAT.json. Lean v4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612. The comparator permits the three listed standard axioms and disables nanoda. No State of Proof build or checker run occurred.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Inspect the fixed-k quantifiers, canonical encoding and concrete machine endpoint, then compare its time and all-prefix space bounds with the manuscript. Keep the manuscript's single-log-log factor and sparse-clause refinement separate from Lean's squared-log-log factor. Select one bounded correspondence check before any isolated replay; no P=NP or practical speedup follows.
Mathematics · Theoretical result · Source record; see version
A manuscript claims that waves cannot stay extremely concentrated for long, with consequences for how line segments can fill space.
Who did it
OpenAI; the manuscript and formalization were produced by an unnamed internal model.
What it could mean
If the argument holds, it would settle major questions about wave concentration and Kakeya geometry across Euclidean dimensions. Practical improvements in imaging or simulation have not been demonstrated.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Compare the Euclidean half-wave, Sobolev and Kakeya definitions with the six Comparator targets; trace one selected endpoint through its source proof before any isolated pinned replay. Preserve finite p, positive ε loss, and strict restriction ranges. Full Hausdorff dimension does not assert positive volume.
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 crest and fan introduce wave concentration and the many directions in Kakeya geometry. These invented forms are not a solution of the wave equation, a time trace, or a Kakeya construction.
Claims the Euclidean half-wave estimate for n≥2 and finite 2≤p<∞, with Sobolev order max(0,(n−1)/2−n/p)+ε for every ε>0; ε=0 is allowed at p=2. Consequences include Kakeya maximal bounds with every positive ε loss, full Hausdorff dimension of every Euclidean Kakeya set, and spherical restriction in the strict conjectured range.
Why this could matter
A limit on how long waves can stay focused A wave can become very intense at one instant. The claim limits that intensity when averaged over time and implies that a set containing a line segment in every direction must have full Hausdorff dimension.
If it holds up
It would resolve major Euclidean wave and Kakeya questions within the stated exponent ranges, giving researchers a common foundation for related Fourier estimates.
If it does not
The failed estimate or formal correspondence would identify where the claimed chain from wave concentration to geometric consequences needs repair.
2026-10-25; October 25, 2026 manuscript; public release at Git commit 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a.
Why we tracked it
source-reviewed intake only; independent examination has not started.
Highest-risk dependency
Analyst judgment: statement correspondence and every dependency connecting the auxiliary partial differential equation to the wave estimate need examination. The six advertised Comparator targets do not certify every additional manuscript consequence. The boundary includes positive ε loss except at p=2, Euclidean geometry, and strict restriction ranges; no State of Proof proof validation or replay has occurred.
Available artifacts
Pinned openai/math 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a; paper.pdf (Git blob 0472605895a485dd0441ada1257485d325f16f55), lean/docs/079.md, lean/OAI/Analysis/Fourier/LocalSmoothing/Comparator.lean and lean/ComparatorChallenges/LocalSmoothing.json. Lean v4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612. No build or checker run in this intake.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Compare the Euclidean half-wave, Sobolev and Kakeya definitions with the six Comparator targets; trace one selected endpoint through its source proof before any isolated pinned replay. Preserve finite p, positive ε loss, and strict restriction ranges. Full Hausdorff dimension does not assert positive volume.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2610.23853
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
Four mathematicians reconstruct a shorter proof of a complex-analysis bound after examining earlier AI-generated manuscripts.
Who did it
Ilia Binder, Oleg Ivrii, István Prause and Stanislav Smirnov; some used AI to understand the earlier work, while this writeup was produced without AI help.
What it could mean
The presented argument could make a major claim easier for specialists to inspect and build on. The stronger strict inequality still awaits its detailed follow-up proof.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Ilia Binder; Oleg Ivrii; István Prause; Stanislav Smirnov.
See the proposed checks
Inspect the critical-point count and signed-area inequality in Section 2.2, then the boundary estimates and uniform limiting passage to general bounded conformal maps in Section 2.3. Treat the non-strict bound as the presented argument; the strict inequality's deferred details require a separate source and 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 two invented surfaces introduce changing shape and boundary distortion. Their grids are illustrative, not an exact conformal mapping, a counterexample or a plotted theorem.
Four specialists present a shorter argument for Bb(t)≤t²/4 for t∈[-2,2], following their examination of earlier OpenAI manuscripts. The paper states a strict inequality on (-2,2) excluding 0, but explicitly provides the full argument only for the non-strict bound and defers the strict-case details.
Why this could matter
Specialists turn an AI proof into a shorter mathematical argument Conformal maps preserve angles but can stretch distances sharply near a boundary. The paper bounds how that stretching accumulates and presents a shorter route to Brennan’s conjectured integrability range. Details of a stronger strict bound are deferred.
If it holds up
The non-strict spectrum bound would provide a shorter foundation for Brennan’s conjecture and a clearer starting point for further complex-analysis work.
If it does not
The signed-area estimate or limiting passage would need repair; the separately deferred strict claim would still require its own detailed proof.
Impact horizon
Foundational · Complex analysis · Conformal maps · Human–AI research
Version
2026-10-16; arXiv v1; submitted October 16, 2026 at 17:59:11 UTC.
Why we tracked it
source-reviewed intake only; independent examination has not started.
Highest-risk dependency
Analyst judgment: the weighted signed-area argument, singularity control and uniform limiting passage need independent examination. Section 1.4 explicitly defers the detailed strict-inequality proof. Do not label that deferred strengthening fully proved by this note, or treat the authors' examination of earlier work as a State of Proof verdict or peer-review status.
Available artifacts
Pinned arXiv:2610.23853v1 supplies PDF, HTML and TeX source. No accompanying code, data or Lean repository was identified in this bounded review. No manuscript code was executed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Inspect the critical-point count and signed-area inequality in Section 2.2, then the boundary estimates and uniform limiting passage to general bounded conformal maps in Section 2.3. Treat the non-strict bound as the presented argument; the strict inequality's deferred details require a separate source and review.
Biology · Experimental finding · Source record; see version
Claude Science, Nathaniel Horwitz, James van Geelen, Kat Kajderowicz and Amir Shanehsazzadeh (as listed in the report)
See the proposed checks
Compare the reported binding classifications with controls, replicate agreement and cross-laboratory measurements, keeping functional outcomes separate from attachment.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The abstract contact surface introduces molecular binding. These invented folds are not actual sequences or structures, and do not show toxin neutralization or antivenom efficacy.
Company technical report with laboratory binding measurements
Evidence reported
Public technical report; Contract-laboratory binding measurements; Released assay data
AI role
An internal Claude model generated protein candidates, helped select candidates for testing, and assisted with analysis and report preparation under human supervision.
Human role
Collaborators selected the research question, targets and prompts and supplemented candidate selection; Adaptyv Bio and Twist Bioscience performed the laboratory measurements.
Source date
; added 2026-10-26
What it claims
The report says 17 of 211 tested AI-designed proteins met its binding criteria against four of five scorpion toxins. No design intended to bind multiple toxins met the criteria against more than one.
Why this could matter
AI-designed proteins pass an early binding test against scorpion toxins Laboratory tests found that some AI-designed proteins attach to scorpion toxins. Such binding can provide a starting point for treatment research, but the study did not establish that these proteins block toxin activity or protect an animal.
If it holds up
Independent researchers gain starting points for testing whether the observed binding can translate into useful toxin inhibition.
If it does not
Repeat measurements or functional tests would show which reported attachments are assay-dependent or fail to affect toxin activity.
Impact horizon
Enabling · Protein research · Neglected diseases · Experimental evidence
Version
Technical report dated October 20, 2026; no numbered version stated; fixed publisher PDF locator
Why we tracked it
An October 20 technical report makes initial laboratory results and the underlying measurement data inspectable.
Highest-risk dependency
No neutralization, animal efficacy or patient benefit was tested. Recombinant toxin activity was undocumented, affinity estimates are preliminary, and assay controls and surface effects limit interpretation.
Available artifacts
Publisher technical report and https://huggingface.co/datasets/Anthropic/scorpion-toxin-binder-design at revision 0bac3d0286f7f83b5339f5b4f1e67fbe47a6e7c1 (October 20), CC BY 4.0. Released measurements include binding results and sensorgrams. This intake contains no sequences or experimental instructions.
Current boundary
Intake record only; examination not started. Company technical-report intake; peer review and independent replication are not established here. Binding is not toxin neutralization. This work does not establish an antivenom, safety or clinical efficacy. Independent examination has not started.
Biology · Research method · Preprint
Candidate · added · biorxiv-2026-10-15-759436
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
A study distributes interpretation of a mouse-brain experiment across thousands of agents and compares the resulting reports with existing findings and expert judgments.
Who did it
Researchers at Scripps Research, OpenAI, PerturbAI, UC San Diego and HHMI, with blinded biological expert reviewers.
What it could mean
Could help scientists extract more testable questions from experiments they have already performed, while keeping the supporting observations visible.
Examination not started · source-reported evidence
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. The source reports the evidence below; State of Proof has not independently reproduced the work.
Alexander Sun, Joshua J. Park, David DeTomaso, Seoyeon Kim, Amelia Liu, Suyash Shringarpure, Kenny Kim, Patrick C. Thompson, Tuo Shi, Yunyun Wang, Eran A. Mukamel, Grace X. Y. Zheng, Y. Joy Jiao and Xin Jin
See the proposed checks
Inspect held-out-data and literature-leakage controls, a fixed sample of claim-to-data links, and the scope of expert comparisons before considering prospective evaluation.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The brain and panels introduce parallel interpretations of a mouse-brain dataset. All cellular forms, dot patterns and atlas panels are invented illustration; none are source data or newly validated mechanisms.
GPT-Rosalind-5.5 agents interpreted individual perturbations, searched literature and assembled evidence-linked explanations and follow-up priorities.
Human role
Researchers generated the mouse-brain experiment, designed the analysis and evaluation, and recruited biological experts to assess reports.
Source date
; added 2026-10-26
What it claims
The authors report that 1,946 agents interpreted a mouse-brain perturbation atlas, recovered 48 of 55 source findings directly supported by the supplied expression data, and generated reports preferred in 45 of 60 blinded paired expert judgments.
Why this could matter
Finding the next question inside millions of brain-cell measurements Dividing a large brain-cell dataset among agents can help scientists connect each gene disruption with earlier research. The resulting reports may help them choose focused experiments, but recovered findings and expert preferences do not establish that new biological explanations are correct.
If it holds up
Researchers could spend less time assembling scattered literature and more time judging which specific biological questions deserve experiments.
If it does not
Independent datasets or prospective tests would reveal where plausible explanations and expert preferences fail to identify useful biological leads.
Impact horizon
Methods · Biological data interpretation · Experimental prioritization · Neuroscience
Version
bioRxiv v1; posted October 16, 2026; announced by OpenAI October 21
Why we tracked it
The October 16 preprint and October 21 announcement fall within this catch-up window. The DOI contains October 15, but the official posting date is October 16.
Highest-risk dependency
Retrospective recovery and expert preference do not confirm new mechanisms. Generalization needs independent datasets and prospective experiments; estimated human effort is not measured human performance.
Available artifacts
Versioned bioRxiv manuscript; https://github.com/jinlabneurogenomics/distributed_agent at observed commit 75a0ed7defc92853ab789a0e571784b9ec2a5999 (October 24) supplies reports, corpus tooling and analysis notebooks; its software and documentation are MIT-licensed. Underlying atlas: https://huggingface.co/datasets/perturbai/wholebrain_crispr_atlas, CC BY 4.0. No code or data analysis executed here.
Current boundary
Intake record only; examination not started. Preprint intake only; independent examination and replication have not started. The output is a set of research leads, not established disease mechanisms, treatments or clinical benefits.
Physics · Mathematics · Theoretical result · Preprint
Candidate · added · 2610.27294
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
A mathematical-physics paper presents counterexamples to uniqueness from ground-state density and total current.
Who did it
Andre Laestadius and Mihály A. Csirik, with disclosed Codex and Claude assistance and a public Lean development.
What it could mean
Could clarify which information and assumptions a magnetic density-functional theory needs; the result does not invalidate density-functional theory as a whole.
Examination not started · source-reported evidence
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. The source reports the evidence below; State of Proof has not independently reproduced the work.
Compare the manuscript counterexamples with the formal statements, inspect the explicit background hypotheses, and distinguish globally defined potentials from the interacting monopole setting.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The paired clouds introduce non-uniqueness under opposite magnetic fields. These invented distributions are not the paper's exact wave functions, a simulation or measured electron densities.
Manuscript constructions and derivations; Public Lean formalization with explicit background assumptions
AI role
The authors disclose using OpenAI Codex and Claude to develop proofs and derivations and to assist with exposition, calculations, references and formal verification.
Human role
Andre Laestadius and Mihály A. Csirik present the constructions, specify their mathematical scope and take responsibility for the manuscript.
Source date
; added 2026-10-26
What it claims
The authors give three two-fermion constructions in three dimensions with the same ground-state density and zero total current but opposite nonzero magnetic fields. Two are noninteracting; the interacting example uses monopole fields and spatially patched potentials.
Why this could matter
The same density and current can conceal different magnetic fields Different magnetic fields can produce the same particle density and total current in these proposed two-particle examples. If correct, the constructions limit a particular rule for reconstructing fields from measurements and help researchers identify which additional assumptions it needs.
If it holds up
Researchers gain explicit examples showing where a proposed uniqueness principle needs additional conditions or a narrower domain.
If it does not
Review would identify whether a spectral argument, a domain interpretation or a formal assumption prevents the proposed pair from being a counterexample.
Impact horizon
Foundational · Mathematical physics · Density-functional theory · Formal verification
Version
arXiv v1; submitted October 19, 2026 at 21:09:56 UTC
Why we tracked it
An October 19 preprint supplies explicit counterexamples, a substantive AI-use disclosure and a versioned formalization with stated assumptions.
Highest-risk dependency
The interacting example uses an enlarged class of magnetic connections. Lean assumes stated background results in operator theory, analysis and geometry; the reported dependency check does not discharge those hypotheses or establish manuscript correspondence.
Available artifacts
arXiv v1 and https://github.com/ERC-REGAL/mag_hk/tree/v1 at commit ca7e200054aae749910bd7f80c48f6362d152ce7 (October 19). Lean v4.34.0-rc2 and mathlib 85e3a25e006c35636f0e53b0e9296caca2685bc0 are pinned. Formalization and coverage/assumption records are public; no build executed here.
Current boundary
Intake record only; examination not started. Preprint intake only; independent proof examination has not started. The formalization is conditional on explicit background results, and the interacting construction must not be generalized beyond its stated magnetic setting.
Physics · Research method · Preprint
Candidate · added · 2610.22367
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
Andi Gu, Alek H. Kemeny, Susanne F. Yelin and Mikhail D. Lukin
See the proposed checks
Inspect task contracts, test distributions, allowed failure probabilities and reconstructed baselines; map the supporting formal lemmas to the circuits that rely on them.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The compact and denser assemblies introduce circuit resource accounting. They are invented sculptures, not executable circuits, hardware results or an observed quantum advantage.
Circuit resource accounting; Programmatic tests under stated task contracts; Released supporting Lean formalizations
AI role
Claude proposed and revised reversible circuit programs using evaluator feedback; researchers report limited human steering between search rounds.
Human role
Researchers defined eight tasks, baselines, resource objectives and correctness evaluators, then presented and interpreted the resulting constructions.
Source date
; added 2026-10-26
What it claims
The authors report lower Toffoli-gate and qubit counts in seven of eight circuit tasks, plus a new resource trade-off for prime-field modular inversion, using LLM proposals evaluated against explicit computational tasks.
Why this could matter
Smaller circuit routines could reduce the cost of future quantum calculations Quantum calculations can require costly operations and extra working qubits. These circuit designs report savings for selected routines, potentially reducing the resources needed by larger algorithms. They do not demonstrate a useful calculation on quantum hardware.
If it holds up
Algorithm designers gain reusable circuit constructions and clearer choices between gate cost and working qubits.
If it does not
A mismatch in error budgets, input distributions or baseline reconstruction could narrow or remove the reported savings.
arXiv v1; submitted October 15, 2026 at 17:59:20 UTC; announced by Anthropic October 16
Why we tracked it
The October 16 announcement is recovered after the monitoring outage. The manuscript was submitted October 15 and is not presented as a newly posted October 19-26 paper.
Highest-risk dependency
Some tasks permit small failure probabilities. Exact gate accounting and random-input checks are distinct from end-to-end correctness; Lean covers selected supporting results, not every circuit or hardware implementation.
Available artifacts
arXiv v1 and https://github.com/andigu/uncompute at commit 64b5a13aa249f1360846657392e6c66817b26d0f (October 16), Apache 2.0: circuits, task definitions, evaluator and supporting Lean proofs. No circuit, evaluator or proof build executed here.
Current boundary
Intake record only; examination not started. Preprint intake only; independent examination and reproduction have not started. Reported resource improvements do not establish hardware performance, practical quantum advantage or a timetable for useful quantum computing.
Examine controls and causal scope, including endogenous versus overexpressed protein evidence, before proposing an independent replication.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The image introduces cellular exchange and material recycling. It is not microscopy, a TM184C structure, or a claim about a particular transfer mechanism.
Mining AlphaFold2 predicted structures helped identify GPCR-like protein candidates.
Human role
Researchers tested localization, molecular interactions, intercellular exchange and autophagy in experimental systems.
Source date
; added 2026-10-15
What it claims
Structure-guided searching nominated TM184C; the authors report cellular and biochemical evidence linking it to intercellular exchange and regulation of autophagy.
Why this could matter
AI points toward an overlooked way cells exchange cargo Predicted structures can nominate proteins for experiments that investigate what cells do. The study informs basic biology; it does not demonstrate a therapy or clinical benefit.
If it holds up
Researchers gain a functional lead for studying cellular exchange and autophagy, and another route into poorly annotated proteins.
If it does not
Independent experiments would clarify which functions depend on the tested systems or experimental assumptions.
Impact horizon
Foundational · Cell biology · Protein function
Version
Nature version of record
Why we tracked it
A September experimental paper added as background for the cross-disciplinary collection; not newly published today.
Highest-risk dependency
Structure similarity nominates candidates; functional conclusions depend on experimental controls and model systems. Clinical benefit is untested.
Available artifacts
Journal manuscript, source data and supplementary material; no experiments reproduced by State of Proof.
Current boundary
Intake record only; examination not started. September peer-reviewed study added as historical context; independent examination and replication have not started. Predicted structure and experimental findings are distinct evidence types.
Physics · Research method · Peer reviewed
Candidate · added · 2609.01705
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
Patrick Reichherzer, Gianluca Gregori, David N. Hosking and Subir Sarkar
See the proposed checks
Reproduce one simulation comparison, including variance and higher moments, against a conventional test-particle baseline.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The spreading cloud introduces transport and a variance-based schedule. The envelope and field lines are conceptual, not measured data or a reproduced simulation.
A diffusion model learns distributional shape while a known variance law sets its schedule.
Human role
Researchers specify the physical law and compare simulations and laboratory measurements.
Source date
; added 2026-10-15
What it claims
The authors anchor a diffusion model's schedule to a known transport variance law and report agreement with particle simulations and a laboratory-measured variance scale.
Why this could matter
Teach AI the physics before asking it to simulate Known physics can provide a physical clock for a learned particle-transport surrogate. Matching variance does not ensure every feature of the distribution or microscopic dynamics is correct.
If it holds up
Researchers could build transport surrogates with a meaningful clock and fewer arbitrary schedule choices.
If it does not
Higher moments or untested transport regimes would reveal the surrogate's limits.
Impact horizon
Methods · Particle transport · Scientific simulation
Version
Nature Communications version of record
Why we tracked it
The journal article appeared October 8; its preprint dates to September 1.
Highest-risk dependency
Enforcing the variance does not enforce full distributions, finite propagation speed, memory or trajectory correlations.
Available artifacts
Journal manuscript, figures and linked availability statements; no source code or data executed by State of Proof.
Current boundary
Intake record only; examination not started. Peer-reviewed method recorded from its source; independent examination and reproduction have not started. No new physical law or practical fusion gain is established here.
Biology · Research method · Preprint
Candidate · added · biorxiv-2026-10-09-758053
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
Review the held-out comparison, uncertainty and generalization limits; retain high-level, non-procedural coverage.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
The highlighted interface represents candidate selection at a high level. These are invented molecular forms, not actual sequences, protein structures or an experimental design.
Experimental training libraries; Prospective held-out transcript test
AI role
Machine learning ranks candidate target sites for RNA sensors.
Human role
Researchers generated training libraries and performed prospective laboratory tests.
Source date
; added 2026-10-15
What it claims
The authors report improved RNA-sensor target-site selection using experimental libraries and a machine-learning ranking method, evaluated on a held-out transcript.
Why this could matter
Fewer dead ends when designing molecular sensors A ranking model could reduce trial and error when choosing sensor targets. The reported laboratory comparison does not establish clinical performance or a diagnostic product.
If it holds up
Researchers could test fewer unproductive sensor candidates before finding a working design.
If it does not
Additional transcripts would reveal where target-site rankings fail to generalize.
A new October 12 preprint with a prospective laboratory comparison; the DOI's October 9 component is not its posting date.
Highest-risk dependency
Preprint findings may not generalize beyond the tested transcripts; clinical sensitivity, specificity and patient outcomes were not established.
Available artifacts
Versioned bioRxiv manuscript and linked supplementary material; no laboratory reproduction by State of Proof.
Current boundary
Intake record only; examination not started. Unreviewed preprint intake; independent examination and replication have not started. Laboratory sensor selection is distinct from clinical validation.
Physics · Capability benchmark · Preprint
Candidate · added · 2610.16733
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
A benchmark asking AI agents to solve 50 unpublished, research-level physics calculations with checkable answers.
Who did it
A. Ramesh Chandra and collaborators, with specialist problem contributors.
What it could mean
Could reduce time spent on specialist calculations if the performance repeats beyond this test.
Examination not started · source-reported evidence
See the check plan
Evidence & validation
From announcement to evidence
A benchmark reports performance on a particular test. Read the problem selection, scoring method and limitations before treating a score as a scientific advance.
The three physical motifs introduce specialist calculation tasks and answer comparison. The curves are invented illustration, not benchmark measurements or evidence that any derivation is correct.
Numerical final-answer comparison; Released evaluation prompts
AI role
Agents attempted calculations with local tools and, on the realistic track, web search.
Human role
Experts supplied problems and reference answers; researchers designed the evaluation.
Source date
; added 2026-10-15
What it claims
The authors report 49/50 correct final answers for GPT-6-Astra with Codex on 50 expert-supplied theoretical-physics calculations with tools available.
Why this could matter
AI takes on the calculations working physicists actually do Reliable calculation assistance could let researchers explore more questions. These tasks test extensions of known techniques, with one full run per agent and final-answer grading.
If it holds up
More researchers could obtain useful specialist calculations with less time and expense.
If it does not
Repeated tests would expose where final-answer accuracy overstates reliable research assistance.
Impact horizon
Methods · Theoretical physics · Research assistance
Version
arXiv v1
Why we tracked it
A recent benchmark of specialist calculations, with separate tool-enabled and web-disabled tracks.
Highest-risk dependency
One run per agent, possible literature memorization and answer-only grading limit generalization; this does not demonstrate breakthrough discovery.
Available artifacts
Manuscript, problem collection and evaluation configuration; no State of Proof reproduction executed.
Current boundary
Intake record only; examination not started. Source-reviewed benchmark intake; independent examination and reproduction have not started. A correct final answer does not validate every derivation.
A benchmark of 82 unresolved literature problems, with proposed answers assessed by four models.
Who did it
Zhiyi Li and collaborators working across mathematics and theoretical physics.
What it could mean
Could help select promising attempts for expert review if the models' judgments survive independent checks.
Examination not started · source-reported evidence
See the check plan
Evidence & validation
From announcement to evidence
A benchmark reports performance on a particular test. Read the problem selection, scoring method and limitations before treating a score as a scientific advance.
The paths and comparison lens introduce alternative attempts and their evaluation. No shape denotes a solved problem, measured score or certified proof.
Models attempt open problems, and four evaluator models judge the proposed answers.
Human role
Researchers assembled literature problems and designed the evaluation scheme.
Source date
; added 2026-10-15
What it claims
The authors assemble 82 unresolved mathematics and theoretical-physics problems, using four evaluator models; the highest reported mean model-judged solve rate is 14.0%.
Why this could matter
AI tries open science—with an important judging caveat A benchmark may reveal useful approaches to unresolved problems. Model agreement can share errors, so its judged solve rate is a hypothesis for independent review.
If it holds up
Researchers gain useful candidate approaches and a test bed for studying progress on unresolved questions.
If it does not
Independent checks would expose shared judging errors and improve how claimed progress is measured.
Impact horizon
Methods · Scientific evaluation · Open problems
Version
arXiv v1
Why we tracked it
An October benchmark makes the distinction between model judgments and independently checked solutions especially visible.
Highest-risk dependency
Evaluator models can share mistakes; judged success does not establish a solved problem or a correct proof.
Available artifacts
Versioned manuscript and benchmark materials; no independent solution verification executed.
Current boundary
Intake record only; examination not started. Benchmark intake only; independent examination has not started. The 82 problems are not 82 resolved discoveries, and model consensus is not proof.
Physics · Mathematics · Theoretical result · Preprint
Candidate · added · 2603.04735
Conceptual illustration · not experimental data, a reproduction, or a proof certificate
Michael P. Brenner, Vincent Cohen-Addad and David Woodruff
See the proposed checks
Pin the integral and assumptions, inspect one analytical route and reproduce a bounded numerical comparison.
Independent examination not started
Peer review, simulation comparisons, laboratory evidence and independent replication are distinct. Inclusion here does not establish all of them; see the record’s source and current boundary.
Calculating radiation from a hypothetical cosmic string
The loop and ripples introduce a theoretical radiation calculation. They do not depict an observed cosmic string, measured signal or a reproduced solution.
Gemini Deep Think explored analytical approaches within tree search and numerical feedback.
Human role
Researchers specified the problem and search framework and presented the mathematical derivations.
Source date
; added 2026-10-15
What it claims
The authors report analytical methods and large-N asymptotics for an integral governing cosmic-string gravitational radiation, found with Gemini Deep Think, tree search and numerical feedback.
Why this could matter
Gemini helps untangle the mathematics of hypothetical cosmic strings Analytical calculations can sharpen predictions of radiation from hypothetical cosmic strings. The result concerns a mathematical model and does not show that cosmic strings exist.
If it holds up
A clearer analytical calculation could make this theoretical model easier to evaluate and compare with numerical predictions.
If it does not
Checking assumptions and asymptotics would show where the proposed analytical route breaks down.
A March background example added to this cross-disciplinary collection in October; it is not a new October announcement.
Highest-risk dependency
Assumptions, singular limits and asymptotic regimes require mathematical review; numerical agreement alone is insufficient.
Available artifacts
Versioned manuscript with derivations, search setup and numerical comparisons; no independent replay executed.
Current boundary
Intake record only; examination not started. March preprint added as historical context; independent examination has not started. Neither a certified derivation nor evidence that cosmic strings exist.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2610.15370
Conceptual illustration · not a proof, verification record, or measured matrix instance
A paper claims one tiny 4-by-4 binary pattern defeats every polynomial bound in a particular matrix-removal problem.
Who did it
Zinan Wang.
What it could mean
If the construction and its formalization hold, they would expose a sharp limit on how efficiently one can force certain ordered matrix patterns to disappear by editing entries.
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 map the stated 4×4 pattern, host construction, induced-copy count, and arbitrary-edit lower bound from the manuscript; then separately inspect the supplied Lean statement and its correspondence to the claimed ordered-removal conclusion in an isolated environment.
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 small ordered pattern spreads through larger grids
The highlighted four-by-four grid introduces the paper's fixed binary pattern; the branching grids conceptually represent its explicit larger hosts. This does not show a counted construction, an edit-distance calculation, or a proof.
The paper claims a fixed 4×4 binary pattern whose induced ordered removal bound is not polynomial. Its construction has order (14h+2)2^h, exact editing distance 2^(2h), and an induced-copy density that decays exponentially in h; the author reports a Lean formalization and verification sources as ancillary files.
Why this could matter
A tiny grid resists every polynomial repair bound Removal questions ask whether a pattern that appears rarely can be eliminated with a proportionally small edit. This paper claims a four-by-four exception: even a very sparse appearance can still demand far more repair than any polynomial rule allows.
If it holds up
It would give combinatorics a smaller, explicit obstruction and a precise target for studying the limits of ordered removal theorems.
If it does not
A failed count, edit lower bound, or formal correspondence would locate which step cannot support the claimed obstruction.
Impact horizon
Foundational · Combinatorics · Extremal matrix theory · Formalized mathematics
Version
arXiv v1; 2026-10-11.
Why we tracked it
source-reviewed mathematical intake, not a validated counterexample, peer review, or homepage feature.
Highest-risk dependency
Analyst judgment: exact induced-versus-non-induced definitions, the quantifier in the removal bound, the host construction, and the source-to-Lean correspondence are load-bearing. The reported formalization does not by itself establish that its endpoint matches every informal claim.
Available artifacts
arXiv v1 lists Lean formalization and verification sources as ancillary files. No local artifact, Lean project, manuscript script, or ancillary file was executed in this intake.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: First map the stated 4×4 pattern, host construction, induced-copy count, and arbitrary-edit lower bound from the manuscript; then separately inspect the supplied Lean statement and its correspondence to the claimed ordered-removal conclusion in an isolated environment.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2610.08893
Source-derived schematic · exact entries, not a full-paper certificate
An explicit table of 86 rows and columns claims to fill a missing case in a family of remarkably balanced mathematical patterns.
Who did it
Harshit Verma. Computer search is reported; AI involvement is not established.
What it could mean
Sometimes progress is an object nobody had managed to build. This one would supply a new, precisely balanced arrangement of signs, with equivalent graph and geometric forms—not an established engineering breakthrough.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Transcribe the printed bit encoding twice independently; check entry conditions, symmetry and C²=85I with exact arithmetic, then inspect the graph conversion. Treat descendant counts as a separate computation.
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.
This source-derived diagram reconstructs the matrix from Section 2's printed bit encoding and border vector. Each tile is an actual entry, not decorative filler. The picture alone is not a proof of the paper's other claims.
Theorem 1.1 claims the specified matrix exists. Equations (2.1–2.2) provide its finite encoding; Lemma 2.1 gives integer identities implying C²=85I. Theorem 3.3 reports ten isomorphism classes among the matrix's 86 descendant graphs.
Why this could matter
An elusive pattern finally comes with every piece Take 86 rows of positive and negative signs. Different rows must cancel perfectly when compared. The paper gives a concrete proposed construction, so this existence claim can be tested with exact arithmetic rather than an enormous search.
If it holds up
The order-86 existence case closes, giving researchers a concrete example and related graph and vector configurations.
If it does not
A transcription or construction error would need locating; a failed example alone would not prove that no such matrix exists.
source-reviewed mathematical intake, not a completed peer review or homepage feature.
Highest-risk dependency
Analyst judgment: correct bit order, circulant orientation and border reconstruction are essential; a copied encoding error can mimic a failed theorem. An explicit witness supports a finite verification route, but no verification was performed here. The construction does not classify every graph with those parameters.
Available artifacts
Section 2 prints a 12-by-12 array of seven-bit values and a border vector specifying an 86-by-86 integer matrix. No author-linked program was executed. A separate local exact-arithmetic witness check is retained for examination; this intake is not a full-paper verdict.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Transcribe the printed bit encoding twice independently; check entry conditions, symmetry and C²=85I with exact arithmetic, then inspect the graph conversion. Treat descendant counts as a separate computation.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2610.08144
Conceptual illustration · not a mathematical verdict
A paper separates a computer-checked proof from a faithful translation of the original mathematics, gives precise complexity results, and reports mismatches in a Navier–Stokes formalization.
Who did it
Alexander Bastounis, Fabian Circelli, and Anders C. Hansen.
What it could mean
A proof checker can give the right answer to the wrong question. This work puts that translation risk under the microscope; it does not declare the Navier–Stokes result false.
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 altered shape illustrates a change of meaning between an informal argument and its formal version. It is not one of the paper's specific Navier–Stokes estimates and does not depict a disproof.
For l≥2 and k≥9, Theorem A.4 claims Σl⁰-completeness for deciding existence of a natural-number witness to the explicitly constructed polynomial predicate. Sections 2–3 distinguish theorem checking from faithful translation of an argument and report specific Navier–Stokes correspondence mismatches.
Why this could matter
Did the computer prove the thing we actually meant? A machine can verify every step after an assumption quietly changes. The paper examines that gap between ordinary mathematics and formal code. Its authors explicitly stop short of deciding whether the original Navier–Stokes proof is correct.
If it holds up
Proof reports would need a clearer bridge between the human claim, formal assumptions, and actual machine-checked conclusion.
If it does not
The particular theorem or mismatch examples would need revision; checking what a formal statement means would still matter.
source-reviewed mathematical intake, not a completed peer review or homepage feature.
Highest-risk dependency
Analyst judgment: avoid turning a worst-case computability result into a claim about every finite translation; independently assess what each reported mismatch implies for the final theorem. The authors expressly do not decide the correctness of OpenAI's natural-language proof. A proof of a correctly specified endpoint can remain valid despite a different derivation; correspondence and theorem validity are separate questions.
Available artifacts
arXiv v1 supplies the manuscript and precise comparisons against OpenAI/NavierStokesAndEuler f9e8bc5b38b6e212696e8a30e3e91517af887bbd. The cited examples and Appendix A theorem have not been independently adjudicated here.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Review A.4's quantified predicate and reduction, then inspect each cited manuscript statement against its exact Lean declaration and downstream uses.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2610.06783
Conceptual illustration · not a proof or benchmark
Algorithms claim to beat two long-standing speed barriers: finding three numbers that sum to zero and calculating shortest paths between every pair of points.
Who did it
Josh Alman and Virginia Vassilevska Williams; core algorithm discovery credited to an internal Claude model, with later formalization by Anthropic.
What it could mean
A crack in two famous speed limits could reshape what researchers think computers can do efficiently. The gains are theoretical and tiny; faster maps or logistics software have not been demonstrated.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Inspect Lemma 11's shared-leaf count and the complete encoding/decoding costs, then the exact reductions and the word-RAM statement. Map the five endpoints and their definitions through both Comparator configurations. Any future replay needs fresh isolated clones, the pinned toolchain, and both Lean and nanoda checks; none occurred here.
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 uses sparse tripartite graphs with a much smaller middle group. The highlighted triangle introduces its algorithmic mechanism, not an executed search, weighted instance, or runtime measurement.
Theorem 22 claims deterministic 3SUM in O(n¹.9992), and min-plus product/APSP in O(n².99942), for polynomially bounded integer inputs; APSP excludes negative cycles. Theorem 19 gives Exact Triangle in O(n².9983). Corollary 39 gives Zero-Weight k-Clique in O(n^(k−0.0017 floor(k/3))).
Why this could matter
Two famous algorithmic speed limits may have cracked Imagine discovering a shortcut where computer scientists had expected a hard limit. These algorithms claim small asymptotic improvements on two cornerstone problems. Because many other problems are connected to them, the consequences could spread well beyond the original questions.
If it holds up
Researchers would revisit conditional speed limits built on 3SUM and shortest paths, and test where the new technique travels.
If it does not
The failed estimate, reduction, or formal correspondence would locate which speedup needs repair—not show that every faster algorithm is impossible.
source-reviewed mathematical intake, not a completed peer review or homepage feature.
Highest-risk dependency
Analyst judgment: the claimed saving must survive every encoding, pruning, tiling and reduction overhead, including uniformity in input magnitude. Source-to-formal correspondence is a separate gate from the correctness of the formal inference. Keep the abstract's rounded APSP exponent 2.9995 distinct from Theorem 22's sharper 2.99942. Integer-input formal endpoints do not certify the paper's separate real-input Las Vegas claims.
Available artifacts
A Lean development is pinned at anthropics/formal-math e1a4e6508154ea59f030480661590a9fe3018011, under 3sum-apsp, with Lean 4.33.1 and five named integer-input endpoints. Real-input running times and Section 5.1 are outside those formal endpoints. No State of Proof Lean or Comparator replay has been completed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Inspect Lemma 11's shared-leaf count and the complete encoding/decoding costs, then the exact reductions and the word-RAM statement. Map the five endpoints and their definitions through both Comparator configurations. Any future replay needs fresh isolated clones, the pinned toolchain, and both Lean and nanoda checks; none occurred here.
Mathematics · Theoretical result · Source record; see version
Pin repository release and Lean/mathlib versions; inspect named theorem statements and axioms; compare encoded assumptions to GAP semantics, with a separately authorized isolated build if needed.
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.
Keeping one position fixed while rearranging others introduces a stabilizer. The paper formalizes selected permutation-group algorithms in Lean. These objects illustrate the idea, not an execution trace or verified output.
The three-page paper reports 35 machine-checked theorems across four modules, selected stabilizer-chain and partition algorithms, and residue-ring results. This overdue intake does not claim verification of every GAP algorithm or its implementation.
Why this could matter
Checking the machinery behind permutation-group calculations Computer algebra depends on routines that sift permutations through stabilizer chains. This work reports Lean proofs for selected routines and their invariants, making their mathematical behavior inspectable rather than relying only on tests.
If it holds up
It would provide a reusable formal base for selected permutation-group and partition-search computations.
If it does not
A mismatch in assumptions, definitions, or the release build would reveal which claimed algorithmic guarantee is narrower than advertised.
Impact horizon
Methods · Computational group theory · Computer algebra · Formalization
Version
submitted 2026-09-29 20:21:25 UTC
Why we tracked it
unexamined mathematical formalization intake, not a proof verdict or homepage feature.
Highest-risk dependency
BSGS completeness assumes complete transversals; the ring cardinality result is representation-specific. Zero-sorry and deterministic-build claims remain author reports.
Available artifacts
gap-lean4-port release v0.2.0 at https://github.com/pCwOrM/gap-lean4-port and related Zenodo DOI 10.5281/zenodo.23045504. No build, axiom examination, or correspondence check was run.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Pin repository release and Lean/mathlib versions; inspect named theorem statements and axioms; compare encoded assumptions to GAP semantics, with a separately authorized isolated build if needed.
Mathematics · Theoretical result · Source record; see version
This seven-edge loop illustrates what a rainbow seven-cycle means. The paper studies the color budget for much larger dense graphs. This simple loop is not the extremal construction, certificate, or proof.
The manuscript claims the asymptotically least palette for graphs with n vertices and at least floor(n²/4)+1 edges in which every seven-cycle is rainbow. The lower bound is new; this is an overdue source recovery, not an October publication.
Why this could matter
The missing seven-cycle case finds its color count Color a dense graph so every seven-edge loop uses seven different colors. The paper claims the least possible palette grows like one eighth of the square of the number of vertices.
If it holds up
It would settle the remaining seven-cycle case at the stated edge threshold and add a Lean-checkable route for the combined odd-cycle statement.
If it does not
A failed certificate or reduction would locate where the proposed lower bound stops reaching arbitrary eligible graphs.
Impact horizon
Foundational · Extremal graph theory · Combinatorics · Formal proof
Version
submitted 2026-09-29 16:35:06 UTC
Why we tracked it
unexamined source-backed theorem intake, not an independent proof verdict or homepage feature.
Highest-risk dependency
The asymptotic statement depends on the exact edge threshold and fixed cycle length. Reported Lean and certificate artifacts are not independently validated here.
Available artifacts
Exact rational certificate/verifier and Lean 4 development reported at https://github.com/Asad-Shahab/erdos-809-lean, described at commit 7ec4aaa. No artifact downloaded or run.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: examination the five-vertex exact certificate, theorem-to-Lean correspondence, and reductions from weighted palettes to arbitrary eligible graph colorings; preserve prior k≥4 attribution.
Mathematics · Theoretical result · Source record; see version
The rulers illustrate a quantity staying fixed while its numerical description changes units. The paper gives formal conditions for conversions to preserve meaning. This is not a numerical conversion table or a tested engineering system.
The typed calculus characterizes surviving rescaling invariance with conversions, checks finite unit declarations, and gives a first-order drift procedure that can certify, name a factor, or decline. This is overdue source recovery, not a deployed-software claim.
Why this could matter
When meters become feet, what stays true? A calculation can appear dimensionally sound yet change its answer when conversion factors change. This paper claims exact rules for when unit-aware programs keep their meaning, and a checker that can flag dependence or decline.
If it holds up
It would extend dimensional-analysis theory to a calculus with conversions and give a Lean-mechanized route for checking its stated invariance and factor-declaration results.
If it does not
A counterexample would show where conversion, declaration consistency, or a claimed invariance condition needs a narrower rule.
unexamined mathematical theorem intake, not a proof verdict or homepage feature.
Highest-risk dependency
Conversion invariance is conditional on coherent rescaling; consistent declarations may still be insufficient to determine a factor. No external workflow guarantee follows.
Available artifacts
Lean 4 mechanization reported at https://github.com/ericeallen/lambda-s; repository and evaluator not downloaded or run.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Map named theorems to Lean declarations; inspect no-unit-constant, positive-factor, nonzero, first-order and decline assumptions; check exact factor extraction.
Mathematics · Theoretical result · Source record; see version
A paper tests a way to translate ordinary mathematical questions into Lean statements while checking whether the meaning survived.
Who did it
Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wenping Deng, and Liang Zhang.
What it could mean
If the method proves reliable beyond its tests, formal proof projects may catch a dangerous error earlier: checking a perfectly typed statement that asks the wrong question.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wenping Deng, and Liang Zhang.
See the proposed checks
Separate answer-aware/agnostic regimes and pass@1/pass@4; examination a fixed informal/formal sample for missing hypotheses, changed bounds, vacuity, and answer injection.
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 matching shapes suggest preserving a mathematical statement while translating it into a formal language. Sage checks statement fidelity; the illustration does not show a proved theorem or a verified benchmark outcome.
A four-stage translation and model-based correction loop reportedly reduces answer leakage in stated evaluations. Compilation uses a single sorry placeholder and does not prove the target. The authors report 71.1% agreement in a 45-case stratified human examination. This is intake of the revised v2 source.
Why this could matter
A proof checker can accept the wrong question Lean can verify that a statement is well formed without knowing whether it matches the mathematician's original problem. Sage adds semantic review to the translation step and reports fewer guessed answers in its tests.
If it holds up
It could improve the quality of formal problem statements supplied to proof assistants, while leaving proof and semantic judgment as separate tasks.
If it does not
Judge disagreements or leaked answers would expose which translation checks still let a wrong formal question look credible.
revised 2026-09-30 11:57:05 UTC; v1 submitted 2026-09-16 17:17:13 UTC
Why we tracked it
unexamined proof-method intake, not a validated semantic gate or homepage feature.
Highest-risk dependency
Model-based semantic judgment is not kernel verification; human-examination agreement is limited, and existential targets can admit proof shortcuts.
Available artifacts
arXiv v2 PDF/HTML/TeX available; no pinned implementation repository established in this pass, and no code/corpus run.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Separate answer-aware/agnostic regimes and pass@1/pass@4; examination a fixed informal/formal sample for missing hypotheses, changed bounds, vacuity, and answer injection.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.30263
Conceptual illustration · not a threshold measurement or proof certificate
A paper claims threshold and random-containment bounds for set families whose overlap complexity is bounded by VC dimension.
Who did it
Chong Shangguan.
What it could mean
A broad threshold conjecture gains a precise bounded-complexity case, with consequences for when random samples are likely to contain structured subsets.
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 definitions of (pc), (q), (qf), VC dimension, and spread; trace the threshold inequality and its constants through the random-containment result; then verify exactly how the robust-sunflower conclusion uses those 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 overlapping ovals suggest a family of sets; the scattered points suggest elements that can belong to several of them. The image introduces bounded-VC set systems and random containment. It is not a measured threshold curve, simulation, or proof certificate.
The inspected abstract states a threshold-versus-expectation-threshold bound for bounded-VC set systems, says this proves Talagrand's integral--fractional conjecture in that regime, and derives stated random-containment and robust-sunflower consequences. It is a current theorem claim about structured set families, not an independently checked general allocation or learning result.
Why this could matter
When structured families cross a random threshold A set family can be complicated, yet still have limited ability to realize every membership pattern. This paper claims that bounded complexity controls how dense a random sample must be before it contains one of the family’s sets.
If it holds up
It would verify Talagrand’s integral--fractional conjecture for fixed VC dimension and sharpen the mathematical toolkit for threshold and sunflower questions.
If it does not
The failure would isolate which complexity, probability, or threshold comparison needs a narrower hypothesis.
Impact horizon
Foundational · Combinatorics · Probability · VC dimension
Version
submitted 2026-09-24 17:59:39 UTC
Why we tracked it
a fresh, source-backed combinatorics theorem with an explicitly named conjectural consequence and robust-sunflower application. Intake does not independently establish the threshold comparison, optimal logarithmic factor, or sunflower derivation.
Highest-risk dependency
The claimed conjecture resolution is limited to bounded VC dimension. Treating the result as a general threshold theorem, or importing the random-family statements into a different combinatorial model without their definitions, would overstate the source.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source for a 20-page manuscript. The inspected record identifies no formal proof assistant, executable implementation, certificate, or repository. No artifact was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the definitions of (pc), (q), (qf), VC dimension, and spread; trace the threshold inequality and its constants through the random-containment result; then verify exactly how the robust-sunflower conclusion uses those hypotheses.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.30261
Conceptual illustration · not a plotted spectral gap or proof certificate
Source-lock the surface class, exponent range, essential-resonance convention, and (epsilon) qualification; map the claimed Fractal Uncertainty Principle and cited two-ends input to the spectral-gap conclusion; test no generalization beyond the stated (delta) interval.
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 funnel suggests convex co-compact hyperbolic geometry; the bright irregular ends suggest the fractal structure named in the paper’s uncertainty-principle route. The bands evoke resonances. This is a conceptual introduction, not a plotted spectral gap, simulation, or proof certificate.
The inspected abstract supplies a gap formula for a stated interval of (delta), its (delta=1/2) specialization, and names a new Fractal Uncertainty Principle as the route. This is a narrow theorem about convex co-compact hyperbolic surfaces, not a generic claim about physical spectra or engineered systems.
Why this could matter
A fractal route to a spectral gap Some curved surfaces have infinitely many long-lived resonant patterns. This paper claims a definite gap separating the leading behavior from the rest when the surface’s fractal boundary has a specified dimension.
If it holds up
It would add a new Fractal Uncertainty Principle and the stated quantitative spectral-gap result under its exact hyperbolic assumptions.
If it does not
The broken step would clarify whether the uncertainty estimate, its geometric input, or its resonance transfer needs revision.
Impact horizon
Foundational · Spectral theory · Hyperbolic geometry · Fractal analysis
Version
submitted 2026-09-24 17:59:34 UTC
Why we tracked it
a fresh, source-backed spectral-theory theorem with a specific geometric regime and proof-method claim. Intake does not independently establish the new uncertainty principle, its dependence on the cited two-ends Furstenberg theorem, or the spectral-gap transfer.
Highest-risk dependency
The numerical (1/64) value applies only after the paper's exact normalization and (delta=1/2) specialization. A statement about a broader surface class or a physics interpretation would not follow from the inspected abstract.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source for a 40+ epsilon-page manuscript. The inspected record identifies no formal proof assistant, executable implementation, certificate, or repository. No artifact was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the surface class, exponent range, essential-resonance convention, and (epsilon) qualification; map the claimed Fractal Uncertainty Principle and cited two-ends input to the spectral-gap conclusion; test no generalization beyond the stated (delta) interval.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.28447
Conceptual illustration · not an exact volume calculation
A paper claims the sharp largest-ellipsoid-volume bound after any halfspace cut through the ellipsoid’s center.
Who did it
Zhou Longfei, Haijun Zou, and Tianhao Liu.
What it could mean
A clean geometric slicing rule may become both mathematically settled and formally checkable, clarifying how much of a maximally inscribed ellipsoid can survive a central cut.
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 exact halfspace, ellipsoid-center, and volume conventions; trace the abstract's positive-definite-matrix reduction, directional rank-one estimate, and sharp circular-cone family; then separately inspect the linked Lean theorem statement and its imports in an isolated environment.
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 blue ellipsoid represents the largest one that fits inside a convex body. The transparent plane represents a halfspace boundary through its center. This image introduces the paper's central-cut geometry; it is not an exact volume calculation, sharp cone family, or proof certificate.
The inspected abstract states a dimension-uniform sharp bound for central halfspace cuts of the maximum-volume inscribed ellipsoid, says an AI language model discovered the proof in a human-directed process, and reports Lean 4/mathlib verification of the main theorem, sharpness, and supporting results. It is a concrete theorem plus a claimed machine-checkable route, not a general-purpose optimization claim.
Why this could matter
A central cut meets a sharp ellipsoid limit Every convex shape has a largest ellipsoid that fits inside it. This paper claims a universal limit on how much of that ellipsoid remains after slicing through its center—and says the bound cannot improve.
If it holds up
It would settle Khachiyan’s conjecture with a sharp, dimension-independent geometric inequality and a reported Lean verification route.
If it does not
The failed reduction or sharpness argument would identify which geometric condition needs repair.
a fresh source-backed convex-geometry theorem with an explicitly named Lean 4/mathlib formalization. Intake does not independently establish its matrix reductions, spectral bounds, sharpness family, or formal-artifact correspondence.
Highest-risk dependency
The sharp constant depends on the precise normalization and central-cut hypothesis. A Lean claim or a spectral inequality excerpt cannot by itself establish that the formal statement matches every geometric condition and sharpness assertion in the manuscript.
Available artifacts
arXiv links a Lean 4/mathlib formalization. No repository, TeX source, Lean project, theorem declaration, or proof script was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the exact halfspace, ellipsoid-center, and volume conventions; trace the abstract's positive-definite-matrix reduction, directional rank-one estimate, and sharp circular-cone family; then separately inspect the linked Lean theorem statement and its imports in an isolated environment.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.11912
Conceptual illustration · not a specific election result
A paper claims every approval-based committee election has a stable, group-fair committee, found in polynomial time.
Who did it
Patrick Becker, Matthias Greger, and Dominik Peters.
What it could mean
A question about whether a group can always be fairly represented may gain an unexpected affirmative answer and a concrete method for finding the committee.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Patrick Becker, Matthias Greger, and Dominik Peters.
See the proposed checks
Source-lock the approval, blocking, and core definitions; trace the entropy-like objective and proof that each local optimum lies in the core; inspect how local search and the stated polynomial bound are obtained without changing the election model.
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 groups suggest voters with different approvals; the central seats suggest a selected committee. The contours evoke the paper's entropy-like objective. This image explains the stability idea, not a computed election, a proof certificate, or a result for a particular electorate.
The inspected abstract says every approval-based committee-election instance has a core committee and presents a polynomial-time method through an entropy-like objective over committees and payment systems. The authors report GPT-6 Astra obtained the proof; Epoch independently identifies this manuscript as resolving its counterexample task. The manuscript's source date remains September 10; this is a September 25 recovery intake, not a new release.
Why this could matter
Every approval election may have a stable committee Voters can form groups that prefer another committee. The paper claims there is always a committee no sufficiently entitled group can jointly block, and gives a method to find one efficiently.
If it holds up
It would settle a central existence question in approval-based multi-winner voting and supply a polynomial-time constructive route.
If it does not
A counterexample or gap would clarify which fairness rule or local-search step breaks.
Impact horizon
Enabling · Social choice · Algorithms · AI-assisted proof
Version
submitted 2026-09-10 17:57:06 UTC
Why we tracked it
a source-backed theorem and constructive proof method, now reconciled to Epoch AI's announcement. Intake does not independently establish the objective, local-optimum argument, or polynomial-time complexity claim.
Highest-risk dependency
The theorem's stability and complexity conclusions depend on exact blocking inequalities, committee size, payment-system definitions, and the claimed local-search structure. A benchmark announcement cannot substitute for checking those formal dependencies.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source for a 20-page manuscript. The inspected sources do not identify a proof-assistant package, executable implementation, or certificate release. No artifact was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the approval, blocking, and core definitions; trace the entropy-like objective and proof that each local optimum lies in the core; inspect how local search and the stated polynomial bound are obtained without changing the election model.
Mathematics · Theoretical result · Source record; see version
A paper claiming several singularity results for carefully defined simplified fluid-cascade models, with two proof approaches.
Who did it
Alexey Cheskidov, Mimi Dai, and Stan Palasek
What it could mean
If its stated model-specific theorems hold, they would clarify how energy cascades can produce singular behavior in those models—not establish the corresponding result for full Navier–Stokes.
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 exact dyadic equations, intermittency and initial-data hypotheses; map each theorem to its stated model and regularity class; then inspect the Lyapunov and multiscale constructions separately. Any numerical illustration is not a substitute for the analytic 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.
Large and small eddies stand for scales in simplified cascade models. The paper studies both inverse transfer and a forward-cascade blow-up mechanism. This picture introduces that idea; it is not a numerical flow field or a solution of the full Navier–Stokes problem.
The inspected abstract and HTML state several singularity/nonuniqueness results for defined dyadic models, including a no-force finite-time result near a stated intermittency parameter, and distinguish a conjecture for true Navier–Stokes equations. Its explicit model boundary and two proof approaches make it timely scrutiny material alongside the recent, separate Navier–Stokes attention cycle.
Why this could matter
What simplified cascades reveal about fluid breakdown Fluid equations move energy across scales. This paper claims that several deliberately simplified cascade models can concentrate that energy into singular behavior, while keeping the model assumptions and proof routes visible for inspection.
If it holds up
It would sharpen the mathematical map of which cascade mechanisms can cause breakdown in the paper’s defined dyadic models.
If it does not
A failed model, regularity, or energy step would show precisely which claimed cascade route does not support the singularity conclusion.
a fresh, source-backed collection of model-specific blow-up claims with two described proof routes. It is not a new proof of the full Navier–Stokes Millennium problem, and intake does not independently establish any theorem or comparison to another manuscript.
Highest-risk dependency
A blow-up theorem for an altered dyadic model does not settle a corresponding statement for the full three-dimensional Navier–Stokes equations. The paper itself labels a true-equation statement as a conjecture; model, forcing, energy, and regularity distinctions are load-bearing.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source for a 35-page manuscript. The inspected record identifies no formal proof assistant package, executable code repository, certificate, or data artifact. No manuscript artifact was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the exact dyadic equations, intermittency and initial-data hypotheses; map each theorem to its stated model and regularity class; then inspect the Lyapunov and multiscale constructions separately. Any numerical illustration is not a substitute for the analytic argument.
Mathematics · Theoretical result · Source record; see version
A constructive method that aims to decide two modal logics by returning either a proof or a finite counterexample.
Who did it
Marianna Girlando, Roman Kuznets, Sonia Marin, and Lutz Straßburger
What it could mean
If the corrected proof-search method holds, it gives researchers a concrete way to turn a yes-or-no logical question into inspectable evidence either way.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Marianna Girlando, Roman Kuznets, Sonia Marin, and Lutz Straßburger.
See the proposed checks
Inspect the exact sequent system, loop-rule soundness/completeness conditions, termination argument, and finite-countermodel extraction; compare the corrected result precisely with the cited LICS 2023 formulation. Any executable proof-search replay must be independently implemented or source-locked in an isolated environment.
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.
One branch suggests a proof; the other suggests a finite countermodel. The proposed decision procedure returns one or the other for formulas in IS4 and IK4. These shapes are an illustration, not a proof or countermodel for a particular formula.
The abstract and conclusion say the procedure decides IS4 and IK4 by returning a proof of validity or finite countermodel, using loop rules in proof search, and that it fixes a mistake in the authors’ LICS 2023 contribution. A concrete proof/countermodel-producing method is a current, inspectable advance in the doing and checking of formal mathematics.
Why this could matter
A logic question gets either proof or counterexample Some mathematical statements are true in every allowed model; others fail somewhere. This paper claims a procedure that does not merely guess: for two specified logics, it returns a proof of truth or a finite model showing failure.
If it holds up
It would add a reusable proof-search pattern for deciding stated intuitionistic modal logics while making both positive and negative answers inspectable.
If it does not
A broken loop rule, termination argument, or countermodel construction would pinpoint why the promised decision procedure needs repair.
a newly posted, source-backed constructive proof-search method with an explicit correction to an earlier contribution. Intake does not independently establish the loop rules, completeness argument, or correction.
Highest-risk dependency
The advertised procedure depends on treating possibly unsound loop rules within a globally sound proof-search organization. A local rule reading, or a changed intuitionistic/modal frame convention, would not establish decidability or the finite-model claim.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source for a 26-page manuscript. The inspected primary record did not identify a Lean, Coq, Isabelle, proof-search implementation, certificate package, or repository. No artifact was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Inspect the exact sequent system, loop-rule soundness/completeness conditions, termination argument, and finite-countermodel extraction; compare the corrected result precisely with the cited LICS 2023 formulation. Any executable proof-search replay must be independently implemented or source-locked in an isolated environment.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.24849
Conceptual illustration · individuals and a collective model
A theorem about when a finite collection of unlike, noise-exposed decision-makers can approximate an idealized crowd model.
Who did it
Aqib Ahmed
What it could mean
If the stated assumptions hold, the work would quantify when a simplified continuum model remains faithful to a finite, heterogeneous control problem—and when its error becomes visible.
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 stated coefficient, kernel, common-noise, and finite-type assumptions; reproduce the finite/continuum system definitions and trace Theorem 3.4 through the feedback and cellwise-coupling steps. Compare the asserted rate only against models satisfying the same information and regularity 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.
Different particles suggest agents with different characteristics; the smooth field suggests their continuum approximation. A shared disturbance represents common noise. The paper bounds approximation errors under specific assumptions; the image is not a simulated population or an observed convergence result.
The abstract derives an exact finite-dimensional stochastic Riccati system for non-exchangeable agents, gives quantitative convergence of the complete backward system to a continuum model, and claims a projected decentralized strategy whose optimality gap vanishes under specified regularity and approximation conditions. It is a current mathematical result about retaining heterogeneity in a controlled multi-agent limit, not a demonstrated operational system result.
Why this could matter
When a crowd model still fits unlike agents Mathematicians often replace many interacting decision-makers with one smooth “average” population. This paper claims error bounds for that shortcut even when agents differ and share unpredictable noise, under a carefully specified linear–quadratic model.
If it holds up
It would give control theorists a sharper way to judge when continuum approximations and decentralized policies are reliable for the paper’s stated finite-agent setting.
If it does not
The failure would expose which heterogeneity, noise, or approximation assumption makes the smooth crowd picture misleading.
Impact horizon
Enabling · Control theory · Stochastic systems · Multi-agent mathematics
Version
submitted 2026-09-21 16:27:55 UTC
Why we tracked it
a fresh, source-backed control-theory theorem with explicit heterogeneity and common-noise assumptions. Intake does not independently establish the backward-system estimates, coupling, or decentralized optimality claim.
Highest-risk dependency
The convergence and optimality claims are conditional on a precise stochastic-control model; treating the continuum limit, representative-agent projection, or (N^-1/2) rate as a generic result for arbitrary heterogeneous autonomous systems would overstate the source.
Available artifacts
arXiv provides PDF, experimental HTML, and TeX source for a 49-page manuscript. The inspected record identifies no formal proof assistant package, executable solver, data release, or certificate artifact. No manuscript artifact was downloaded, executed, or replayed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Source-lock the stated coefficient, kernel, common-noise, and finite-type assumptions; reproduce the finite/continuum system definitions and trace Theorem 3.4 through the feedback and cellwise-coupling steps. Compare the asserted rate only against models satisfying the same information and regularity conditions.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.22077
Conceptual illustration · not exact optimal coordinates
A paper identifies a square antiprism as the claimed best eight-point arrangement for several spherical energy models, with Lean-checked proof components.
Who did it
Liudmyla Kryvonos, Lukas Liehr, and Mitchell A. Taylor
What it could mean
If the stated formalization and certificates hold, they show how a delicate computer-assisted optimization proof can be made inspectable in a proof assistant. This does not settle energy minimization for arbitrary numbers of points.
Examination not started
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Liudmyla Kryvonos, Lukas Liehr, and Mitchell A. Taylor.
See the proposed checks
Inspect the repository pin, Lean toolchain and certificate inputs in an isolated environment; trace Theorems 1.1–1.3 through the exact energy definitions and certificate statements. Do not execute manuscript-linked artifacts in this intake run.
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 proposed minimizing shape has two squares rotated relative to one another. Their separation depends on the energy being studied. This illustration shows the square-antiprism idea, not the exact optimal coordinates or a computer-verified configuration.
The inspected abstract and HTML Theorems 1.1–1.3 claim that a square antiprism is the unique global minimizer for eight points under logarithmic and Coulomb energy, establish a sufficiently-large Riesz-exponent result, and state a Lean-verified computer-assisted route for the first two. The explicit proof artifacts and formalization make this a direct contribution to checking mathematics.
Why this could matter
Can eight points find their lowest-energy arrangement? When repelling points share a sphere, geometry decides the least-energy pattern. This paper claims that, for stated energy laws, one eight-point square antiprism wins uniquely—and makes key proof components checkable in Lean.
If it holds up
It would supply a reproducible formal-checking route for a precise global-optimization result in discrete geometry.
If it does not
A certificate, formalization boundary, or energy-family assumption would reveal exactly where the proposed optimality claim needs repair.
a fresh primary-source theorem/formalization record with a concrete Lean and certificate route. Intake does not independently validate the formalization, certificates, or the claimed all-exponent extension.
Highest-risk dependency
The scope is eight points and stated energy families. The abstract distinguishes Lean-verified results from an additional computer-assisted all-exponent route; neither may be generalized to arbitrary point configurations or potentials.
Available artifacts
arXiv exposes PDF, HTML and TeX; Section 9 names a companion Lean development and finite certificates at github.com/lukasliehr/Energy-Minimization-8-Points. No artifact was executed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Inspect the repository pin, Lean toolchain and certificate inputs in an isolated environment; trace Theorems 1.1–1.3 through the exact energy definitions and certificate statements. Do not execute manuscript-linked artifacts in this intake run.
Mathematics · Theoretical result · Source record; see version
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 unequal stretching suggests Kasner geometry; the disturbance suggests a perturbation of it. The paper analyzes growing and non-decaying modes at the linearized level near the Big Bang. This is not a picture of the actual early universe or a nonlinear simulation.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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 paper describes generating non-pyramidal polyhedra from a square pyramid using specified graph transformations. The highlighted pieces suggest local changes. This image introduces the construction idea; its shapes are not an exact sequence of the paper’s operations.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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 two colors suggest opposite signs. Each overlapping group collects some of those contributions, making simultaneous balance a mathematical challenge. The picture illustrates discrepancy, not a computed coloring, a numerical bound or proof of the paper’s claims.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
In a weighted tree, the distance between two vertices is the sum along their unique connecting path. The paper claims that the required all-distinct distance pattern is impossible for an 18-vertex Leech tree. This is a generic tree illustration, not such a configuration or a search certificate.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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 puzzle is not just filling a square: the integer rectangles must also satisfy a pairwise incomparability condition. The paper claims 27 is the smallest possible side length. The illustration shows the packing idea, not the certified 27-by-27 arrangement or evidence for minimality.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.19118
Conceptual illustration · selection under constraints
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.
Opportunities arrive one at a time, but a choice must respect which combinations are allowed. The paper studies selection guarantees under precise matroid and arrival assumptions. The slots are an intuition, not a representation of every matroid or a promised improvement for real scheduling.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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 central axis suggests the symmetry studied by the paper. Its regularity result depends on specified asymptotic symmetry, growth bounds and analytic forcing. This illustration is not a computed solution, a general no-blow-up claim or a refutation of other Navier–Stokes constructions.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
Candidate · added · 2609.20805
Conceptual illustration · frequency building blocks
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 waves suggest functions assembled from exponential building blocks. The paper establishes a completeness claim for specified frequency sets and function spaces. The image does not show a finite exact reconstruction, numerical experiment or practical compression algorithm.
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Which quantitative estimates and interval certificates are complete, and which stability obligations are still open?
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Does the upgrade from spatial smoothness to joint space-time smoothness hold uniformly, and where does the new argument depend on prior work?
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Does the formal endpoint establish the same smooth-data, whole-space, unforced theorem as the paper?
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Are the force's space-time smoothness and the stated uniqueness class preserved throughout the analytic-to-formal translation?
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Do both forcing terms remain smooth through blowup, and do the formal hypotheses match the paper's localized solution class?
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Verify even/odd dimensional scope, exact support, and both positive-definiteness assertions; highest risk is the function-class and distance-kernel correspondence.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Available artifacts
None linked from the arXiv record.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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 claimed surface result explicitly identified as part one of two.
Highest-risk dependency
a two-paper dependency.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Map the exact generalized surface statement and wait for/source-lock the companion paper; highest risk is a two-paper dependency.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Map coherence, continuity, fibre realization, and sheaf-model notions to the original problem; highest risk is a mismatch between the construction and Kanalas' hypotheses.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
fresh all-dimensions counterexample to a proposed strengthening, adjacent to the Escobar record but not the same claim.
Highest-risk dependency
whether the proposed strengthening and its function-space hypotheses are precisely those refuted.
Available artifacts
New Slack discovery packet; no formal/code artifact listed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
fresh explicit claimed counterexample; a bounded geometry-and-eigenvalue examination is available.
Highest-risk dependency
simultaneous satisfaction of the geometric hypotheses in the conjecture's exact regime.
Available artifacts
New Slack discovery packet; manuscript says the proof is human-verifiable; no separate formal/code artifact listed.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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 narrowly stated counterexample with an explicit numerical interval and an a-posteriori contraction route; no docket created.
Highest-risk dependency
the numerical-to-exact bridge that establishes a genuine analytic domain and boundary conditions.
Available artifacts
Primary manuscript and TeX source available; the arXiv record did not list a formal/code artifact; no current social signal used.
Current boundary
Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
Mathematics · Theoretical result · Source record; see version
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. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: 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.
This bounded discovery list includes historical context with original source dates. Peer review, simulation comparisons, laboratory experiments and independent replication are distinct evidence states. The separate proof dockets retain their mathematical scope.
