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 30 of 39
Whistler's conjecture proof was developed with Claude and GPT models, and agents later formalized it. The repository does not isolate which central argument in the original paper was supplied by AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source expressly formalizes Stein’s and Bourgain’s maximal theorems using a classical proof route. Agents generated most Lean proof code under human supervision, while the mathematical theorems and route predate the project.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The linked Nikodym repository redirects and its cited formalization disclosure was not retrievable. The title alone cannot establish the origin or exact scope of the sharp exponent.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry formalizes Theorem 1.2 of Zakharov’s previously published human paper. ChatGPT assisted formalization and a revised PDF with a typo correction; no new central AI mathematical claim is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The cited Kronecker–Weber repository revision returned 404, so its exact statement and AI disclosure could not be inspected. The registry title alone cannot establish eligibility or exclusion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Both Li’s criterion and its zero-sum coefficient form are attributed to Li and Bombieri–Lagarias. Claude wrote the Lean machinery under the maintainer’s direction; the disclosure identifies formalization of known results, not a new AI mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The exact OneTwo projection census is in Rudolph’s preprint; cited metadata assigns Sol and Fable formalization and adversarial review, but the original paper’s discovery history was not accessible.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The registered coding statements are Dong–Yang Theorems 1–5. Codex agents discharged Lean proof obligations under human supervision for that prior classification.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Brill–Noether and gonality results are explicitly attributed to earlier named papers. Generative AI primarily created the Lean formalizations, not the mathematical results being formalized.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The return-window results are presented as original, and GPT-family agents built proof modules under Alexander’s detailed direction. The disclosure does not identify whether agents supplied a central construction or executed the author’s mathematical plan.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The bounded Erdős 647 certificate was generated by a Python program and checked in Lean; the authors say they wrote the witness format and proof. The disclosed automation is a deterministic generator and replayer, not central AI mathematical work.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper claims a new K₃,₃,₁-minor redundancy result for tetrahedral balls. Sol and Fable developed the Lean finite and clique-sum layers, but the disclosure does not distinguish their mathematical ideas from Rudolph’s source proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not establish that AI supplied the central all-even-m bit-reversal proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source identifies Tucker’s 1945 lemma and later classical arguments as what the AI workflow formalized.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The lower bound is Bae’s paper result. The original disclosure calls the agent work AI-assisted Lean development under his direction and states that the mathematics is the paper’s, with no formalization novelty claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The radial-harmonic classification and circular-orbit stability analysis are drawn from Ehrenfest and classical potential theory. AI composed Lean proofs under an author-supplied route and statements.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository contains nine different preprints. Its disclosure credits Sol and Fable with formalization and adversarial analysis, but the queue does not identify which preprint each of these four entries represents or a central AI-origin idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository contains nine different preprints. Its disclosure credits Sol and Fable with formalization and adversarial analysis, but the queue does not identify which preprint each of these four entries represents or a central AI-origin idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository contains nine different preprints. Its disclosure credits Sol and Fable with formalization and adversarial analysis, but the queue does not identify which preprint each of these four entries represents or a central AI-origin idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository contains nine different preprints. Its disclosure credits Sol and Fable with formalization and adversarial analysis, but the queue does not identify which preprint each of these four entries represents or a central AI-origin idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This entry points to a repository with nine distinct preprints. The root disclosure credits Sol and Fable with formalization and adversarial analysis but does not identify a central AI-origin contribution for this entry.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Tverberg’s and colorful Tverberg’s theorems are sourced to prior authors. Gemini agents formalized their proofs in Lean under maintainer direction, with no AI-origin theorem identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Hamiltonian-cycle criterion is Ore's theorem; Dirac's condition is its cited corollary. Agents formalized and golfed these classical proofs under maintainer direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The fixed repository README is a Poincaré formalization roadmap and mentions a curvature subproject, but it does not disclose AI’s role in the selected Levi–Civita and curvature claims.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The trace-tensor and signature-product statements are presented as general classical results with concrete instances. Claude agents drafted Lean proofs, but the disclosure does not attribute a new mathematical result or idea to them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Baker–Norine supply the graph Riemann–Roch and Clifford results. Development began manually; later agents refactored, debugged and edited the Lean formalization.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited Heilbronn repository could not be read: the root formalization file returned 404 and the cited tree was unavailable. No original AI/proof disclosure was available to assess.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The record identifies Kőnig, Egerváry, Gallai, and Hall as sources of the selected min–max and matching results. Agentic work formalized those established theorems under maintainer direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
ChatGPT and Codex formalized Gargava–Viazovska’s earlier theorem; the README also reports trace, boundary, and Gamma corrections whose mathematical scope and AI origin are unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalization credits agents with proof development and checking of Rudolph's periodic signing, but does not establish who discovered the period-8 signing or the decisive certificate.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The full-sequence Erdős 625 bound is presented as original and AI assisted its interactive proof, but the human author selected the theorem and the disclosure does not assign the central argument to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project explicitly formalizes the 1948 De Bruijn–Erdős theorem and its near-pencil tightness, with AI used for Lean proof tactics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The target and proof route are Nash's and Günther's established theorem, following Wassermann's notes. The disclosure credits Claude and Aristotle with designing the Lean architecture and supplying formal proof bodies, not with an independent mathematical result or proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared two-sided limit theorem and both named constructions are Salem's 1963 theorem and cases. The cited disclosure says the author fixed those targets and chose the argument route, while Claude drafted and repaired the Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalization records AI-assisted F₂ chain proofs for Rudolph's dense flag-homology counterexample family. It does not say whether AI originated the paper's family or extremal argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Grushko–Neumann rank theorem is classical. AI materially generated Lean declarations and proof scripts; the human authors selected and reviewed the mathematical result and source relation.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared general-n statements draw on classical results, including the published morphic classification and Selmer/Siegel inputs. The disclosure credits Claude with proof drafting and Lean error-loop work under the author’s statement design, not a retained new mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source says this formalization was entirely human-written and follows the established Fourier proof of Arrow’s theorem. Its disclosure identifies no AI mathematical role.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The decreasing-diagrams criterion belongs to van Oostrom, while this project claims a new finite certificate language, checker boundary and completeness bridge. Codex developed the generic soundness proof, but the disclosure does not separate human design from any retained AI mathematical construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Howson’s finite-rank free-group theorem is the historical source. Codex developed the Lean proof against that target; no distinct AI-origin mathematical result is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Marshall Hall’s and Grushko–Neumann’s results are credited to their original human authors. GPT-5 Codex is credited with Lean proof development against cited APIs, with no new mathematical result assigned to it.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The 2001 morphic-number classification is prior work, but this formalization replaces part of its proof with a mirror-dichotomy argument. Claude drafted proofs under human direction; the disclosure does not establish who devised that distinct proof route.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The native e-graph checker may be a new algorithmic contribution, but disclosure identifies GPT-5 Codex only with proof engineering; origin of the design is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The spectral and Stone theorems follow standard published routes. Claude and Codex built the Lean library and an equivalent publication boundary, but the record does not claim an AI-origin new mathematical theorem or proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository does not expose a root formalization.yaml, so its original claim and AI/proof disclosure could not be checked.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The separable CHSH, witness, Born-rule and Werner claims are traced to cited quantum-information sources. Alexander fixed and reviewed statements; Claude drafted and repaired Lean proofs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The target operator inequalities are established, but the disclosure says the final proof used a different smooth-support outer-approximation route after a proposed lemma failed. The source does not establish who devised that route or whether it is a central new proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The friendship windmill theorem is Erdős–Rényi–Sós’s 1966 result. The agentic workflow formalized it under maintainer direction, with no new AI-origin mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Malliavin and Clark–Ocone statements are established source mathematics; the disclosure credits AI agents with building the Lean proof library, not originating those results.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Dilworth’s and Mirsky’s decomposition theorems are historical source results. The agentic workflow formalized and polished Lean proofs under maintainer direction; no original AI mathematics is disclosed.
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.
