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 29 of 39
The exponential-map theorem and main proof route are from Misiurewicz and Shen–Rempe, with Rempe directing and correcting the formalization. Claude and Codex built Lean proofs, not an original result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The main norm-variation statements and proof organization were written by the human authors in the blueprint. Agents formalized and filled proof details; the metadata does not attribute a new central result to them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The disclosed result synthesizes classical Feller-process and Kolmogorov continuity theory and explicitly disclaims a new mathematical result. Models wrote and audited the Lean development under close human supervision.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared quenched homogenization estimate is expressly a specialization of Armstrong–Kuusi’s 2025 paper. Models wrote Lean code under the paper authors’ close supervision; no new AI-origin mathematical contribution is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The X-ray results are presented as original research from JD Jones’s private notes. Codex assisted mathematical research and Lean development, but the disclosure does not isolate an AI-origin construction or extension idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The README explicitly calls the Carlson results source-based formalizations/adaptations and disclaims a new node-domain extension; AI work is proof writing and debugging.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This formalizes Bae’s earlier Corollary 1.2, and the disclosure describes AI-assisted Lean development only. The paper’s own proof-origin account still needs checking before ruling out central AI work in the original result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project states it formalizes a pre-existing fixed-rank matrix paper; the disclosed AI role is formalization with author-directed review.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The two boundary-regularity theorems are from the cited paper. The human author supplied the goals and proof strategy; AI agents subdivided and formalized those existing arguments.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source adapts Fourier–Jacobi calculations from Paul, Pitale, Saha and Schmidt; the author fixed the explicit-kernel target and agents developed proofs. It does not identify who supplied any new central evaluation beyond the source calculations.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Most results formalize a supplied manuscript, but the disclosure calls the unrestricted-naturality refutation a new classical Lean proof distinct from an unavailable Idris proof. Its AI-origin mathematical idea and novelty need separation.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Robin’s and Lagarias’s RH equivalence criteria and the Nicolas oscillation input are explicitly credited to their original papers. The maintainer designed the theorem targets; Codex assisted with Lean proof development.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The MI-32 conjecture is proved through an agent-assisted informal draft, and the Lean proof replaces two draft steps. The disclosure does not isolate whether agents originated a central new argument or implemented the author’s proof plan.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The bowtie-boundary results appear to be new, and Codex substantially assisted proofs, but the disclosure says the human selected scope and does not identify who found the central removal or composition argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This is a source-based formalization of Kong–Zeng’s permutohedron paper and earlier reduction. AI agents divided implementation and auditing, but the disclosure does not credit them with the mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source says an earlier submission was withdrawn and revised materials were not resubmitted, while the registry still lists the earlier version. The status of the revised claim is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Unpublished human notes may contain the decisive invariant and quadratic-extension argument; the source does not isolate the AI-origin mathematical step.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The assigned mathlib4 repository moved and its cited formalization disclosure could not be read. The title names an older Broughton–Huff theorem, but that alone is insufficient to exclude the entry or establish an AI-origin contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author’s disclosure says people select and specify each theorem while Claude generates Lean statements and proofs. This entry formalizes the Kolmogorov–Arnold representation theorem rather than attributing its mathematical origin to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This is an independent Lean proof of the classical Bonnet–Myers theorem, with no new mathematical priority claimed. AI work is described as proof engineering and verification under human-selected scope.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The classification follows David Gale’s established outline. The source records human-written development and only some ChatGPT-generated lemma proofs, which does not document an AI-origin central mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript and native proof record supply the prime-cover graph result. The disclosure assigns agents proof implementation, porting and verification under a human mathematical specification, with no central AI-origin result documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source explicitly calls this a mechanization of Dann et al.’s 2025 counterexample families and disclaims independent mathematical novelty. AI assistance is assigned proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected results are Tsuchioka's Kanade–Russell identities. Codex is credited with constructing Lean proofs and auditing agreement with the source, not with originating the identities or a distinct central mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source presents Rudolph’s proof of Davila’s zombie-damage conjecture and reports ChatGPT assistance in research and Codex/Claude assistance in formalization and review. It does not identify which central graph or strategy idea, if any, AI supplied.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source combines a classical external-to-swap regret reduction with an explicit RM/RM+ specialization and executable certificates. It calls the latter standalone, but assigns AI only proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The global Stafford extension is presented as an original theorem, but the disclosure assigns mathematical plans to the human author and implementation to agents without identifying the origin of its decisive idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The sharp eigenvalue bound and Obata rigidity are classical results. GPT-5 is credited with Lean proof engineering and audits under the maintainer’s fixed theorem scope, not new mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The explicit rational (23_4) witness may be new. The disclosure says Codex handled human-directed construction and formalization while search and computer algebra aided discovery, but it does not identify who found the coordinates.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The spherical-maximal theorem is Fraccaroli–Roos–Seeger’s source result, with main statements and definitions written by humans. Agents supplied Lean proofs, prerequisites and a blueprint.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The negative stepping-up lemma is an Erdős–Rado result followed through cited expositions. Claude participated in formalization; the disclosure does not assign the underlying order-type argument to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source identifies Farina’s regret-matching and no-regret-to-Nash lectures as the mathematical results formalized. Its AI disclosure assigns GPT-5 Codex proof engineering, with no central new mathematical result credited to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected correlated-equilibrium and regret statements follow Aumann and standard game-theory sources; the disclosure limits GPT-5 Codex to proof engineering of those targets.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The replacement derives the classical double-contracted Bianchi identity from a connection. GPT-6 Codex repaired and formalized the argument after reviewer objections; the disclosed target and identity are established mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The dependent finite-action equilibrium claim represents Nash's theorem with a repository-specific bridge to an existing fixed-point formalization. GPT-5 Codex is credited with proof engineering, without a new mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source presents a new deterministic two-to-one map, but says assistants substantially wrote Lean definitions and proofs from a human-directed manuscript. It does not resolve who devised the map.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The maintainer says he selected and specified the Hoeffding result and read its statement; Claude generated the formal Lean statement and proof. No AI-origin mathematical result is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The record expressly disclaims new mathematics and traces the Nash and potential-game results to prior papers and formalizations. Its AI disclosure assigns proof engineering, not the mathematical ideas, to GPT-5 Codex.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The maximal-difference inequality is presented as established Pietsch s-number theory. Ullrich designed and revised statements; AI produced most Lean proofs. No AI-origin s-number result is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The companion paper and Lean were developed together, but the disclosure says Stephan fixed the targets and that the paper’s mathematical content is his. Claude generated formalization and a prose draft under his direction; no central AI mathematical idea is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Collatz transport theorem comes from Shaik’s manuscript and author-supplied mathematical research and constraints. Codex materially assisted Lean construction and audits, but no central AI-origin mathematics is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source credits Ezzeri Esa with the original Hlawka proof and says the agent received audited mathematical proof artifacts before formalization. AI proof construction in Lean is documented, but central mathematical origin is human.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript claims rr = non(M), and the author says AI-generated proofs were first drafts later verified and refined by him. The disclosure does not isolate whether a central proof idea came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The root disclosure credits Sol and Fable with formalization and adversarial analysis, while the per-project metadata only says AI assistance is disclosed in the paper. It does not establish who found the integer-trade or sharp-grid arguments.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source documents AI ideation and Lean proof work, but does not identify whether AI supplied the central weighted-spectral proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The frozen paper states the rerandomized SRHT result, and the metadata calls AI assistance substantive in mathematical development without identifying a specific AI-origin theorem or proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The mathematical PFR development was written by human contributors from 2023 to 2025. Claude wrote only the Palomar submission files and bridge statements after that development.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The density Hales–Jewett and Szemerédi theorems and density-increment route are cited from earlier work. Agents planned and implemented Lean proofs under author steering; no new central mathematical contribution is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify a retained central Version 4 proof idea or construction supplied by Codex.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The double-contracted Bianchi identity is classical. GPT-6 repaired an earlier Lean formalization by deriving the connection-level identities after reviewer objections, but the disclosure describes a formalization repair, not a new mathematical contribution.
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.
