Sources we considered, with review status and reasons.
3070 recorded entries · 652 awaiting detailed review · 584 excluded · 672 on hold · 3 publisher withdrawals · 1159 related to curated records.
Suggest a missing contribution or correction.
See omissions and decisions reviewed against public discussion.
Entries without a recorded subject appear only under All subjects. Coverage totals describe all subjects.
1911 matching entries · Page 28 of 39
The source reports extensive AI assistance but does not identify whether AI originated a central branch-message or weighted-cancellation proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected weighted-support criterion is original to Cook’s papers, but the entry credits AI with formalization and exposition while the repository describes AI-assisted mathematical research; the origin of the criterion is unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source explicitly calls its Shapley axiomatization a reusable formalization of the 1953 characterization; AI assistance is identified as proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The 52 compared locally convex space theorems are drawn from standard books and papers. The author selected the material and sources while agents wrote Lean text.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify a central existence or diagonal lemma originated by AI rather than supplied in human proof material.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Seifert–van Kampen pushout is the classical groupoid theorem, adapting an existing directed Lean formalization. The agent supplied Lean proof engineering under human scope direction, not a new mathematical theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The exact dimension-five graph results are Chaffee and Noble’s 2016 Theorems 8 and 10. The detailed AI campaign reproduced upstream statements and proved them in Lean; it did not originate the mathematical results.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Favard quarter exponent: pinned source says an unpublished manuscript was produced in a human-directed ChatGPT project and Claude formalized it, but does not allocate the new joint negative-moment idea between human and AI; hold for primary AI-role evidence.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The finite automata theorem and folding construction are attributed to Stallings. Codex developed the Lean proof with human-directed scope; no distinct AI-origin mathematical contribution is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The main extremal graph theorem follows Chaffee–Noble, but Claude constructed hypothesis-drop counterexamples and filled two proof steps omitted from the paper. Their independent mathematical value and centrality are unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalized Collatz density statements come from Shaik’s prior manuscript. The disclosure says the author supplied the mathematical research and plan while agents assembled, extracted and checked Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The zero-density results come from Fiori’s source preprint. AI wrote and checked the Lean formalization and numerical certificate scripts under his work list; the mathematical direction and preprint are his.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The three Caffarelli–Kohn–Nirenberg conclusions are older results, but the manuscript was corrected during agent-assisted proof development. The authors say they decided the mathematics and corrections; the exact AI role in the direct-iteration route remains unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
SCOPE, REACH and their Rao–Blackwell variance argument come from the cited paper. Astra formalized the paper’s estimator statements under a maintainer-specified objective and did not claim to originate them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The private manuscript and available disclosure do not identify whether the central construction came from AI or the human author.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source describes a cooperative improvement without identifying which central support, width or allocation idea originated with AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript reports substantial AI assistance with lemma exploration as well as Lean development, while Pouly directed the research. The disclosure does not identify whether an AI proposed a central new lemma or merely helped develop human ideas.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify which central mathematical step, if any, came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The five main results come from the cited 2025 paper, with a paper author auditing the statements. Claude workers wrote Lean proofs and review artifacts; no new AI mathematical result is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The disclosure expressly calls the no-go theorem human-authored mathematical work. Codex assisted the Lean proof and mechanical audit only.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify which central mathematical step, if any, came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify which central mathematical step, if any, came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The finite-poset bound is a theorem from Jo’s stable-marriage paper. The disclosure reports AI proof exploration and auxiliary lemmas, but says the human author selected the final route; the origin of any central new proof step remains unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Fischer’s 24-vertex graph and its invariants are the source result. AI assistance formalized and audited that known counterexample without claiming a new mathematical construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The exact exterior power-sum lower bound was proved earlier by Luo–Yang–Zhu. This Lean proof follows Tan–Wang–Huang–Chen's residual-polynomial route; generic AI proof-development credit identifies no new AI power-sum idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify which central mathematical step, if any, came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Colbrook’s paper presents a claimed proof of the Kung–Traub conjecture and counterexamples; the disclosure says ChatGPT assisted discussion and checking, without identifying a central AI-originated argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited SparseStack source was not retrievable. The title alone does not establish whether AI found improved constants or only formalized them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper reports substantial AI lemma exploration, drafting and Lean work, but the disclosure does not identify which central Poisson-field or exact-mark result AI supplied. The two registry entries need separate claim-level attribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper reports substantial AI lemma exploration, drafting and Lean work, but the disclosure does not identify which central Poisson-field or exact-mark result AI supplied. The two registry entries need separate claim-level attribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected double-covering theorem follows Chojecki’s Theorem 1.1, but the Lean project replaces a cited Green–Tao step with a direct Fourier proof and reports AI-assisted local research. The originality and AI origin of that replacement need checking.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected improper phi-regret families and reduction barriers come from Dann, Mansour, Mohri, Schneider and Sivan (2025). GPT-5 Codex is disclosed for proof engineering rather than originating the paper’s central mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not separate the AI contribution to the central consistency construction from supporting lemmas and formalization.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The claimed ζ₇(3) irrationality proof is new, and AI was used for mathematical derivations and exploration. Yi Taifeng supplied the proof architecture and repeatedly redirected the work, so the central AI-origin step remains unidentified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected BKAR forest formula is a formalization of the Brydges–Kennedy source, under stronger smoothness assumptions. AI wrote Lean code, but the source does not claim a new formula or construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The supplied human manuscript and notes are not public in the cited snapshot, preventing a line-by-line origin comparison for the central continuous projection estimate.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The record documents substantial AI assistance but does not assign the central convex-body mathematical idea to AI; an involvement level would be speculative.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The 67 compared several-complex-variables statements are sourced to classical treatments, and the exact metadata says none of the results is claimed new. The author selected sources and conventions; AI agents wrote most of the Lean development.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Perassi wrote the working note and its theorem before formalization. Agents wrote and repaired Lean code under his direction; the source does not assign the sharp bounds or equality classification to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The authors' article supplies the statistical reformulation and finite-setting results. Its disclosure limits GPT-6 Astra to Lean proofs and manuscript-to-formalization cross-checking, so no central mathematical discovery is attributed to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected perturbation bounds derive from Yu–Wang–Samworth’s 2015 paper. Agents formalized and audited source defects; the human maintainer adjudicated the corrections. The record does not attribute a new central mathematical result to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Komlós and Beck–Fiala bounds follow Karingula–Lovett’s earlier proof. Claude implemented it in Lean and GPT revised the code under human-directed statement and proof style.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The four selected quadratic-Carleson endpoint claims are identified as Theorems 1 and 2 of Fragkos–Krause–Lacey's original paper. The metadata assigns mathematical scope and statement selection to humans and Codex to Lean development and repository preparation.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The superdiffusion theorems are the Armstrong–Bou-Rabee–Kuusi paper’s results. Models wrote the Lean code under author supervision, but the source does not assign them the original mathematical results.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not establish that all sixteen hypotheses hold together for the claimed geometric resolvent families or that the abstract quantities match the intended invariants.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The centered-xi asymptotic is a new analytic input developed with substantial AI help, but the disclosure does not identify the origin of its saddle-point argument or derivative estimates.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
GPT-6 prepared a formalization of Chang, Liu and Liu’s human proof of Chvátal’s conjecture. The source identifies no retained new AI mathematical contribution beyond formalizing their result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The core chain-bounding results were published in the 2024 paper and first formalized without AI. GLM-assisted work was a later toolchain port and one formalization step, not a new mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript preceded the Lean work and AI agents formalized its statements, but the disclosure does not establish who originated the unpublished classification and obstruction theorems.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected rotation-of-eigenvectors theorem families are Davis–Kahan’s 1970 results. Models assisted source review, interface design and Lean proofs, not the source mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Discovery metadata attribution: What AI Found, CC BY 4.0 · VibeMathed contributors, editorial layer CC BY 4.0. AIProofWatch supplies the screening decisions.
Allow optional Google Analytics to help improve AIProofWatch? Privacy details.
