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 23 of 39
Known compact-Hausdorff countable-network metrization theorem. Formal proof and agent work alone do not establish a new central AI contribution under current policy.
Screening recorded: 2026-10-18 · Decision reviewed: 2026-10-18T07:37:42.537Z
The compositum package includes a claimed canonical-pair witness and new exact identities alongside classical Coxeter material. Claude drafted and repaired proofs, but the original mathematical origin of the claimed new parts is not documented.
Screening recorded: 2026-10-18 · Decision reviewed: 2026-10-18T00:00:00.000Z
Known Nash–Williams–Tutte packing and arboricity results. Formalization and registry admission alone do not satisfy central-AI eligibility.
Screening recorded: 2026-10-18 · Decision reviewed: 2026-10-18T07:37:42.537Z
The cited disclosure says GPT-6 systems assisted mathematical arguments and exact certificate discovery, but it does not identify which central retained idea or certificate came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The exact Recht–Ré counterexamples are new candidates, but the disclosure describes AI assistance across research and formalization without naming a retained central AI construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The claimed sharp bound comes from a private informal manuscript that cannot be checked here. Codex is described as formalizing and packaging it, so the origin and scope of any AI mathematical contribution remain unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Ehard–Glock–Joos theorems are prior work, but this proof replaces their Molloy–Reed step with a trimmed-nibble construction. Aristotle proved from supplied plans and Claude designed/reviewed the route; the origin of that replacement is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source formalizes the classical Sneider Gδ-diagonal criterion, not the cited paper’s new small-diagonal results. Codex authored Lean proofs and tests, with no new mathematical result claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The current package ports an already public counterexample proof and adds a bridge to a corrected global statement. The original archive’s AI/proof origin is not established by this disclosure.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The discrete Carleson theorem and proof are taken from the two cited Krause–Roos papers. AI made a blueprint and Lean proofs for those source arguments, not a new central mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify a central new geometric idea or result supplied by AI beyond human direction and Lean proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected cone square-function theorems come from Cushman–Demeter–Wu. Claude and Codex are credited with autoformalization and proof bridges, not discovery of the source estimates.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Füredi’s and Erdős–Simonovits’s stability theorems are cited as prior results. Aristotle and Claude generated Lean proofs and plans for those established claims, without a new central mathematical contribution documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source presents finite certificates and conservation-only and differentiable-only routes developed in AI-assisted PDT research. Alexander selected the results, but the disclosure does not say whether Codex supplied the central new arguments or only their Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The waist theorems are sourced to Gromov, Memarian and Klartag. Aristotle is credited with assisting their Lean formalization, with no central new mathematical idea identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository says it reproduces a prior AI-assisted Lean proof of Kra–Moreira–Richter–Robertson’s 2024 theorem; this adaptation claims no new mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source expressly calls the Alexandroff–Urysohn criterion classical and claims no novelty. Codex authored the Lean proofs and packaging; that is not a new mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The augmented Descartes and Soddy statements are explicitly formalized from Lagarias–Mallows–Wilks and their cited higher-dimensional proof. Claude’s documented work is source reading, Lean proofs and audits.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Cauchy–Binet, Kirchhoff’s matrix-tree theorem and Cayley’s formula are established results. The author supplied statements and proof plans; Aristotle generated their Lean formal proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Erdős–Gallai and Havel–Hakimi are established characterizations, with Choudum’s sufficiency proof followed. Agent work implements the Lean formalization.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source formalizes classical Euler–Hierholzer and Petersen theorems and explicitly says no mathematical novelty is claimed. Claude wrote Lean code and proposed proof plans approved by the human author; no new central result is attributed to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Gallai–Hasse–Roy–Vitaver theorem is established. The human author chose the result, while Aristotle and Claude generated Lean proofs from supplied formal statements and a proof plan.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected MUB, SIC-POVM, Welch and Gerzon results are mapped individually to earlier papers and formalizations. Claude agents produced Lean proofs and source audits, but the disclosure does not identify a new central mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not distinguish core mathematical statements first supplied by AI from earlier notes or human direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The connected counterexample family is supplied by a private manuscript that cannot be checked against the repository. GPT-6 is credited with Lean proofs and certificates, not clearly with discovering the family.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author says he proved the finite-multiplicity Erdős 99 result himself and gave Aristotle a finished manuscript for Lean formalization. The documented AI work is transcription and proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source credits agents with proof development but does not identify which central classification or periodicity step they originated.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The six selected statements are Evans §6.2 solvability results. Claude wrote and refactored Lean proofs under hand-fixed literature statements; the disclosure does not assign AI a new central result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project explicitly calls itself an attributed Flypitch reproduction of the established CH independence formalization. AI agents adapted and audited existing Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository derives Petersen’s established matching theorem from Tutte’s theorem. The human author chose the statement and proof plan; Aristotle supplied the Lean proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalization adapts a preexisting elliptic-curve manuscript and leaves its prime asymptotic as a hypothesis. GPT-6 agents checked and formalized that target; the disclosure identifies no AI-origin result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry explicitly formalizes classical Mader, Dirac and Hadwiger results and says no mathematical novelty is claimed. Aristotle proved supplied formal statements and proof plans; Claude designed and reviewed them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This package selects Greenwood–Gleason, Erdős–Szekeres, and Erdős graph Ramsey bounds; the author chose the classical results and AI generated Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Kőnig, Kőnig–Egerváry, Dilworth and Mirsky claims are credited to classical sources. The author chose results and routes and supplied statements and plans; Aristotle and Claude generated Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source formalizes Kuratowski’s 1930 theorem through Wagner’s theorem. It explicitly says the human author chose the result and route, supplied proof plans, and claims no mathematical novelty; agents supplied Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository does not expose a root formalization.yaml, so the source theorem and AI/proof disclosure were not readable.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The localized spectral bound is tied to the earlier conjecture and Bradač’s scalar argument, with a reused BN spectral lift. Codex is credited for local Lean adaptation and toolchain port, not for a new central mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The disclosure explicitly says Pranava Kumar devised the common-height mathematical argument without automation. Claude translated that proof into Lean and later agents ported it, so the central result is human-origin.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
AxiomProver generated the Lean proof of Lau’s Collatz density theorem, but the formalization record does not say who supplied the paper’s central mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The three selected results specialize or restate Haxell–Rödl and classical nibble/LP claims; metadata says the human author supplied results and proof plans, AI produced Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The H² lifting criterion is classical, and the human supplied six starting Lean lemmas. Agents completed and compiled this proof and its matrix application without a novelty claim or documented new central mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The strict rational rounding statement and floating-coordinate proof are Beck–Fiala's theorem. Traverso chose the result and route; Claude generated the Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Dross’s published 9n/10 theorem and its max-flow route supplied both the statement and proof plan. Aristotle generated Lean proofs from the author’s plans; no new mathematics is claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project formalizes all numbered statements of Troscheit’s prior Brownian-image paper. Claude and GPT-6 performed Lean proof development and review, with no disclosed AI-origin mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cutoff-826 totient counterexample and strict-pattern consequence are explicitly attributed to Chojecki’s Proposition 1.2. Codex supplied a finite certificate and a bound derived from the absent pattern; the source claims no new result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The registered results are Wagner, Škrekovski, Thomassen, Li–Wang and Voigt theorems. The author supplied the statements, routes and proof plans; Aristotle generated Lean proofs of those established results.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Vizing’s bound and McDiarmid’s equitable refinement are earlier results. The source says the human author chose the results and route while AI generated Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source formalizes the established Häggkvist–Janssen theorem and does not document a new AI-origin mathematical proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project explicitly formalizes classical Smirnov metrization and claims no new mathematics; Codex wrote the formal proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The pinned README explicitly formalizes Grötzsch's and Kostochka–Yancey's established human theorems. The author says he chose the statements and proof route; AI generated Lean code and formal proofs but no distinct central new mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
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.
