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 31 of 39
The selected Schreier and Kurosh statements are the classical subgroup theorems. GPT-5 Codex is disclosed for Lean proof development and checking, not a new central mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected superorthogonality theorem was published in 2024. Codex generated Lean proofs from author-written statements, not the theorem or its mathematical criterion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared finite-dimensional representation and homogeneity results come from Busch’s 2003 theorem. Claude drafted and repaired Lean proofs after the human fixed the statements and targets.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Comparator wrapper follows the Glimm–Jaffe/Osterwalder–Schrader construction and exposes an existing Lean library. Claude, Codex and Gemini are disclosed for proving, coding and packaging, with no new mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The registered result is the classical Kuratowski–Ryll-Nardzewski single-selector theorem, adapted from cited textbook proofs. The disclosure credits Claude with generating Lean code under human direction, not with an original mathematical result or method.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository describes a classical measurable-selection formalization and Bellman representation, but the two generic registry entries are not mapped to distinct selected declarations in the queue. AI generated Lean under human direction; claim-level origin cannot be assigned yet.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository describes a classical measurable-selection formalization and Bellman representation, but the two generic registry entries are not mapped to distinct selected declarations in the queue. AI generated Lean under human direction; claim-level origin cannot be assigned yet.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The registered result is the existing Kuratowski–Ryll-Nardzewski selection theorem, proved by its classical dense-sequence route. Claude generated its Lean proof from a specified target; the Bellman project is outside the selected statement.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The colorful Helly theorem is established, but this formalization extends the cited compact-set statement to arbitrary convex sets using a finite witness-pool construction. The disclosure does not say who devised that extension.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The fair-partition theorem is attributed to Akopyan, Avvakumov and Karasev. ChatGPT and Aristotle helped with proof ideas and Lean development for its formalization, without a documented new central mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The degree-two through four Mahler minimizers and values are credited to Lehmer, Siegel and Smyth. Claude drafted Lean proofs under the author’s design; the compared mathematical claims predate this project.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Frankl–Wilson bound is the 1981 source theorem. An agentic workflow formalized it in Lean with maintainer audit, without an AI-origin mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This formalizes the author’s prime-star spectra manuscript. Codex did theorem decomposition and much Lean implementation, but the disclosure does not resolve whether any central mathematical argument originated with AI rather than the manuscript.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Schreier index formula is classical. GPT-5 Codex is credited for Lean proof development and checking, without a new central mathematical result attributed to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The targets are classical results of Rückert and standard local complex-analytic geometry; Codex implemented and audited Lean proofs under human-fixed mathematical targets.
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 selected Malliavin integration-by-parts and closability statements adapt Nualart’s Hilbert-process theorems to a Gaussian Banach-space setting. Agents helped author the challenge and proof library, but the source does not establish whether the adaptation contains a new AI-originated idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited composition-algebras repository returned 404, so its original proof and AI disclosure could not be read. The repository title alone cannot establish eligibility.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Happy Ending theorem and the stated binomial bound are attributed to Erdős and Szekeres in 1935. The agentic workflow formalized the known result under maintainer direction; the source does not credit AI with a new mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected colorful Carathéodory, selection, and centerpoint theorems are credited to Bárány, Carathéodory, and Rado. The agentic workflow formalized and proof-golfed those established results under maintainer direction; no AI-origin mathematical result is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected classification is the existing Lean Eval surface-classification challenge and follows classical classification sources. The disclosure credits AI with most implementation while humans chose sources, proof strategy and interfaces.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
AI agents formalized the classical Weierstrass theorem; the source does not establish a new central mathematical result or proof idea attributable to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Alpöge supplied the order-668 Hadamard construction payload. The record says Codex translated and checked that supplied certificate in Lean, after an Isabelle check, and claims no discovery of the construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository could not be read (GitHub returned 404), so neither the mathematical claim nor its AI/proof disclosure can be audited.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Radon’s lemma and Helly’s theorem are credited to their original authors. The agentic workflow formalized these established theorems under maintainer direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The quotient-comparison theorem and winding examples are extracted from a prior manuscript. Human mathematical design is disclosed; the AI role is extraction, compatibility repair and Lean proof review.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The new supporting-plane deduction is explicitly Yuhang Shi’s research argument. Codex translated it into Lean and checked the proof boundary; the source does not assign its central mathematical step to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source explicitly says this is a standalone Lean reimplementation of an existing Isabelle/AFP finite counterexample and claims no new mathematical counterexample. GPT-5 assisted proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited campaign describes AI models as co-researchers and lists several Jacobian-conjecture subprojects, but the registry entry’s exact selected claim and model-origin step cannot be identified from the accessible root disclosure.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository source cannot be read: GitHub returns 404 for this commit, so its proof route and original AI disclosure cannot be audited.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected localization-to-UFD implication is Nagata’s theorem, independently formalized by the human authors. The disclosure credits Codex with repository preparation and reproducibility checks, not an originating mathematical argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The three oracle-complexity results are bound to an unpublished manuscript. Codex did proof exploration and Lean engineering, while authors reviewed the mathematics; the disclosure does not identify which central argument, if any, originated with AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The disclosure expressly claims no new mathematics: the author fixed classical coordinate results and AI agents developed Lean proofs and computations against those statements.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The formalization checks Shi’s exact p = 29 counterexample, and Codex assisted proof decomposition and certificate transcription. The original discovery and proof attribution are not resolved by this disclosure.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The split-Levi square-determinant criterion is a specific result of the companion paper. The cited disclosure credits Codex with repository preparation and proof review, without identifying who devised the field-sensitive mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Descartes’s rule and the parity conclusion are attributed to Descartes and Gauss. The agentic Lean workflow formalized and connected these established statements to Mathlib; no new mathematical result is credited to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The mathematical higher-lambda results are credited to Martinez-Rivillas and de Queiroz’s earlier papers. GPT-5 assisted Lean development and packaging, while the repository explicitly separates source authors from the formalization author.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This is the established Sperner parity theorem generalized into an abstract n-dimensional Lean presentation. The disclosure assigns the agent formalization work under maintainer direction, not a new mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This source formalizes the earlier Alpöge–Fable result rather than introducing a separate AI-origin contribution. The original claim needs its own assessment.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The grammar and automata equivalences, hierarchy, and closure results are traced to established sources. The AI roles are described as proof assistance and engineering within human-directed theorem design, with no novelty claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not isolate an AI-origin central mathematical step for either global or prefix claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Hall’s marriage theorem is a classical 1935 result. The disclosure describes an agentic Lean formalization under maintainer direction, with no distinct mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not isolate an AI-origin central mathematical idea for any of the three clauses.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository follows Bourgain–Gamburd–Sarnak, Chen, and Martin but adds a certificate-free explicit cutoff. It credits GPT-5.6 Sol with human-directed formalization and humans with theorem design; the origin of the new cutoff argument is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The NF ⊢ ¬WPP endpoint originates in a project Metamath extension and manuscript, while Codex agents built the standard-NF equivalence and translation bridge. The record does not establish who discovered the original WPP argument or whether the bridge is a distinct central AI result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The free-group description of a finite graph's fundamental group is attributed to Hatcher and Mathlib's existing groupoid machinery. GPT-5 Codex assisted Lean API exploration and proof development, with no claimed new central mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify the central AI-origin mathematical step.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source explicitly credits Yates with the counterexample and says Claude agents worked from his mathematical draft. Their corrections of two wrong formalization specifications do not establish AI origin of the J₉(0) sign anomaly.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source calls the zero-geometry mathematics the author’s work and says Claude agents formalized an existing draft, despite repairing two incorrect specifications. Those repairs do not establish an AI-origin central result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Sylvester–Gallai is a classical theorem with cited historical proofs. The disclosed Gemini-assisted workflow formalized it in Lean under maintainer direction, with no AI-origin mathematical result.
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.
