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 25 of 39
The paper reports five months of AI-assisted work on its main proof, with substantial author revision, but does not identify which central ideas came from AI. The repository chiefly documents AI source development and proof repair.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Neumann claim is separate and plausible, but the cited repository calls itself a pre-submission snapshot while later listings describe the same commit as registered; AI mathematical origin is broad.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The seven-cycle threshold and longer odd-cycle argument are credited to prior human papers. AI systems generated certificates and Lean proofs for those published results, not the result itself.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README/CREDITS credit Mark Lewko with original contribution and Codex with proof development, adaptation, debugging and integration. The AI role in the improved zero-density exponent is not identified as central.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The source does not show that AI supplied a central mathematical idea rather than assisting human-origin arguments and formalization.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalization follows Jaswal’s own preprint and discloses AI use for Lean, but the manuscript’s original mathematical authorship and any AI role are not established here.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not attribute the central mathematical construction or witness search to AI rather than Naslund; the AI contribution remains unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository formalizes a versioned Ginibre Poincaré paper; agents wrote proofs under human-supplied goals. The paper’s proof-origin account has not established a central AI idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The stability, Lieb–Thirring and related estimates adapt cited mathematical sources. The authors chose the scope and proof routes before agents wrote plans and Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The annulus and overlap theorems are Bakaev–Yehudayoff's results. Aristotle reconstructed their proof in Lean; Gemini and ChatGPT aided code and submission work. No separate AI plank-covering idea is credited.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Meyer-space construction comes from a private PR requiring access. The metadata reports AI mathematical agent roles but does not disclose which construction steps originated with them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The sharp propagation theorem is the author’s manuscript theorem. Claude worked on statement design, Lean proof, port and reviews under the author’s mathematical direction; the disclosure identifies no AI-origin mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The factorial-square constructions, prime obstruction and cutoff are expressly classical; the density question remains unproved. Agents supplied an independent Lean proof of selected known supporting results.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository does not expose a root formalization.yaml, and the registry page supplies no readable disclosure here. The theorem’s origin and AI role remain unverified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The strict order arc is presented as a consequence of Kelley's 1942 lemmas. The human selected the target, Codex built the Lean proof, and the pinned record disclaims mathematical novelty.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README says AI made substantive mathematical-analysis contributions but the five-dimensional S54 tile and proof chain came from retained source snapshots with unknown original bibliographic authors. The origin of the central CLARK construction is not resolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The formalization improves Lewko’s v2 bound by saving a linear m term, and Codex assembled the refined bounds. The disclosure does not establish who derived that improvement mathematically.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Alexandroff property is Todorov–Valov Theorem 3.3, with classical composant foundations. Codex formalized an alternative bridge under human-selected scope; no AI-origin mathematical result is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The fifteen submitted balayage bounds come from Lin’s human-authored source proofs. GPT-6 formalized selected statements and the author explicitly directed omission of a harder bound.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Knight supplied the unpublished construction, while later human–AI interaction added unspecified ideas. The record does not identify a retained central idea supplied by AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository goes beyond the Aliev–Rakhuba paper with unitary results, stronger real singularity ranges and four-layer counterexamples. ChatGPT assisted Lean proof development, but the source does not assign these mathematical extensions to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compact-Hausdorff factorization and uniqueness are expressly formalized from Daverman’s stronger theorem. Codex is disclosed for Lean development; no new mathematical factorization is attributed to it.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Catalan/Mihăilescu theorem is a prior proof following Bilu’s cyclotomic exposition. Agents wrote and ported Lean code under the author’s fixed acceptance criteria; no new mathematical result is claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The B_H pinned-distance criterion is Lin’s earlier manuscript Theorem 1.1. Codex is disclosed for submission preparation and audits, while the original proof-development AI history is explicitly undocumented; central AI involvement cannot be determined.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source claims logarithmic gauge nullity and a 25/23 parabolic box bound, but points to local manuscripts. The disclosure names AI proof agents without identifying whether they supplied the central estimates or formalized a human draft.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Both non-cut-point assertions are identified as Proposition 29.3 of a topology textbook. Human direction selected the proof route; Codex agents formalized and checked these established statements.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The countable closed-partition theorem is sourced to the Washington University topology notes. Codex formalized and independently reviewed that established theorem under a human-selected scope.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify a retained central AI-origin step in the protected-reserve improvement.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The component-frontier result is classical boundary bumping, cited to Ball–Hagler–Ormes, with a prior Isabelle formalization. Humans selected the target and Codex constructed the Lean proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository selects the author’s Theorem 1.1 and says Codex assisted proof development, but the source manuscript was pending publication and the retained AI idea is not identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The main superdiffusive and regularity statements are from the cited Armstrong–Bou-Rabee–Kuusi preprint. Agents formalized them and repaired documented paper errors, but the disclosure says the corrections do not change the statements and identifies no separate AI-origin result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Markman’s Hodge-Weil results and arguments supply the mathematical source. The agents formalized and reviewed that paper; the conditional sheaf-theory hypothesis is named rather than an AI-origin result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
No source assigns a specific central new quantitative or aliquot argument to AI rather than the maintainer or inherited work, so AI involvement is unrated.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The exact negative answer to Erdős 958 and its short-arc construction are credited to Clemen, Dumitrescu and Liu (2025). AI-assisted Lean proof development formalized that prior construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The negative answer to Erdős 2 was proved by Hough and later Balister et al.; this formalization follows the latter probability-sieve route. AI worked on Lean proof development and audits.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalization strengthens a textbook fixed-dimension cell-attachment statement to arbitrary mixed dimensions. AI assisted proof construction, but the disclosure does not identify who supplied the generalization or its central argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The arbitrary-family two-cell attachment theorem is expressly classical. AI assistance is assigned to construction of the Lean proof and review, not a new mathematical theorem or idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The sparse graph Ramsey bound is Sudakov’s published affirmative solution of Erdős 546. AI developed and checked a Lean reconstruction of that proof, not a new result or documented new proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected construction extends Chojecki’s parabolic cap to a four-layer signed grid and a sharper constant. AI-assisted proof development is disclosed, but the origin of that new construction is not assigned.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript claims new quantitative RAF critical-window bounds, but the automation record only says AI-assisted Lean development and source migration. Mathematical idea provenance is unspecified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README proves a Gallai path-decomposition subclass and says Codex and Claude assisted mathematical development and Lean work, but does not identify who supplied the central new graph argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The source explicitly formalizes Allman–Degnan–Rhodes’s 2011 species-tree theorem. Claude agents handled formalization, source comparisons and packaging, with no new central mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository formalizes four MIP*=RE results but also describes an alternate low-degree route and source-proof gap; the AI role in that route is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Stafford 3.8 and strengthened bounds are research claims, while the disclosure explicitly says the model list does not assign mathematical authorship. Central AI origin remains unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The bounded FKS claim is expressly said to follow from published results and not to be new. AI agents formalized it from supplied statements and proof plans; no central new AI mathematics is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This is Monderer–Shapley’s classical exact-potential characterization. GPT-6.1 Sol aided primary-source research and Lean proof construction for that source theorem; no new mathematical claim is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source reports Codex and Claude assistance with constructions, counterexamples, stronger cube bounds and grid results, but describes the author as directing the research. It does not allocate the selected central ideas between human and AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Falmagne’s finite random-utility theorem and the flow/Möbius route are credited to earlier papers. The disclosure expressly claims no mathematical novelty; GPT-6.1 constructed and checked their Lean formalization.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected equivalence is Milgrom–Shannon’s 1994 Theorem 4. The disclosure characterizes this as its full Lean formalization and identifies no AI-origin mathematical advance.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
GPT-6 Pro developed proofs from the author’s notes, but the source does not establish whether a decisive proof idea originated with AI or the notes.
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.
