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 26 of 39
The selected regularity theorems and proof routes are established, but the disclosure says models filled gaps in the printed proofs. It does not establish whether those arguments are routine formal details or a central new mathematical proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The finite persuasion result is Kamenica–Gentzkow (2011), with finite splitting and attainment also adapted from Econlib. Codex developed and reviewed the Lean economic model and proof; no new central AI mathematical contribution is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Navier–Stokes statements come from the cited Constantin–Ignatova–Vicol paper. The disclosure explicitly says the human authors decided the mathematics and theorem statements while models wrote the Lean code and proof designs.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository and registry record were not retrievable, so the loose-Hamilton-cycle proof and any central AI role cannot be assessed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned metadata lists Codex model/proof development and AI review but does not identify AI as origin of the binary congruence or sharp frontier; the source itself makes no novelty claim. Resolve mathematical attribution and baseline.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
A central model-origin step is not identified, so the AI-involvement level cannot be assigned without speculation.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry proves variants of the established Cook–Levin NP-completeness theorem in Lean. It documents AI formalization, not a new AI-origin mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The quotient-channel RAF limit is an original result in Mislan’s manuscript. The metadata describes AI-assisted development and packaging without assigning the critical-window argument to AI or the author.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The finite equivalence is Gershkov et al. (2013), including the quadratic lifting route. Codex supplied Lean definitions and proofs for that cited result and AI source review, without a documented new central mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected diffusion statements come from the prior Armstrong–Vicol paper. Models performed Lean development and audits against author-approved statements, with no AI-origin mathematical contribution disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source formalizes Bergemann–Morris but states a zero-prior-mass extension and support handling. AI performed exact proof development; the origin of that extension is not assigned.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected AGV mechanism result is a classical theorem. Codex is credited with source inspection and Lean proof implementation, not with a new mechanism or central mathematical idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This is a Lean presentation of Maskin’s established Nash-implementation theorem. Its source is marked formalizes and no AI mathematical discovery is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This formalizes the 1988 Cremer–McLean theorem and its established side-bet proof. Codex is credited with source inspection and Lean proof implementation, not the mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Metadata screened. Requires original-source review of the specific contribution, baseline and central AI work, with separate AI involvement, technical verification, human understanding and importance ratings before publication.
Screening recorded: 2026-10-26
Pham–Sauermann supply the rearrangement and anticoncentration results. ChatGPT drafted and Claude completed a Lean formalization of their paper, with no AI-origin mathematical result claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The graded near lemma and certificate format appear first in Naslund’s paper. Claude chose Lean statements and proofs to formalize those paper components; the full Linnik bound is outside the formalization, and no AI-origin mathematical result is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared auction-feasibility theorem is Border’s existing finite result, with null-support details matched to his source. Codex performed source inspection and Lean proof implementation; no new central mathematical result is claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The companion manuscript claims a new RAF critical-window law, while the disclosure only documents Codex source migration, metadata and statement packaging. Central AI origin of the limiting-law argument is unestablished.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared cyclic-monotonicity characterization is Rochet’s established result. Codex performed source review and Lean implementation, with no AI-origin central mathematical advance claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected termination, core, and uniqueness results are Gale/Shapley–Scarf top-trading-cycles mathematics. GPT-6.1 generated the Lean development, not the underlying result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The original paper's author specified the recurrence mathematics. The disclosure credits Claude and Codex with writing the Lean development from the paper and auditing finite cases, not with originating the recurrences.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Lengyel's manuscript describes a research result, while the metadata credits AI with mathematical exploration and Lean definitions and proofs but gives no specific AI-origin central idea. The author also corrected scope and representation choices.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The package extends the authors’ bounded-orbit results to derived singular sets, disconnected surfaces and positive-area consequences. AI built formal proofs, but the disclosure also credits Rempe with proof suggestions and does not isolate an AI-originated central extension.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected optimal-auction theorem formalizes Myerson’s 1981 result. The README’s support counterexample and regularity repair correct this project’s earlier statement; the disclosure credits Codex with Lean work, not a distinct auction-theory result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The three selected envelope, payment and expected-revenue equalities are scoped versions of Myerson's 1981 revenue-equivalence theorem. The README credits GPT-6.1 with formalization and packaging and credits Myerson for the mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The target is Morrison's unchanged lean-eval Gleason statement, and its core lemma follows Cooke–Keane–Moran. Claude Code is credited with drafting Lean only.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project formalizes the Green–Laffont characterization and standard finite VCG properties. Its disclosure limits AI assistance to formalization and packaging, with no new mathematical mechanism attributed to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The onto-DSIC affine-maximizer claim is Roberts's 1979 theorem. The proof follows Dobzinski–Nisan's route and Lavi–Mualem–Nisan's tie-breaking reduction; GPT-6 Luna did formalization and packaging.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Bulow–Klemperer revenue comparison is sourced to the earlier auction theorem. GPT-6 assistance is described as formalization and packaging of that comparison.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Burkhart et al.’s 2020 filter theorem and remarks are the mathematical source. Codex adapted an earlier formal proof, added Lean proofs and packaged it; the author reviewed the challenge statement.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Burkhart’s paper predates the selected formalization, which added group identifications and counterexample proofs. The repository’s AI disclosure concerns Lean work; the paper’s own origin account needs checking before exclusion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected finite minimax theorem is von Neumann’s 1928 result. Codex is disclosed for Lean formalization and packaging, without a new AI-origin mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify a central proof idea or construction supplied by ChatGPT beyond the human-selected targets and AI formalization.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source explicitly credits Akopyan and Polyanskii with the short mathematical proof of Ball’s theorem. AI tools assisted Akopyan’s Lean formalization of that human proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README specifies a new two-reaction counterexample and formal proof but gives no documented AI origin of the reaction-network witness.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The manuscript claims new amenability results across coalgebras, Hopf algebras, groups and Lie algebras. Source headers credit ChatGPT-assisted proof development, but the disclosure does not separate AI mathematical ideas from Bartholdi’s manuscript arguments.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The public disclosure does not identify which central adaptive-reciprocal construction or proof step came from AI, and the underlying source is private.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The original C2 research record does not assign the central classifier or field-decoder idea to AI; the AI contribution remains unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The sharp binomial-gcd results are presented as original, and AI assisted mathematical research and proof development. The source does not isolate which central mathematical idea or result AI supplied.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Theorem A is attributed to the cited Bartholdi paper. Aristotle produced its Lean formalization and later agents repaired packaging and toolchain issues; no original AI mathematical work is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project identifies Evertse’s 1984 results and the established Subspace Theorem chain as its mathematical sources. Claude agents generated Lean libraries from human-directed roadmaps; no distinct AI-origin theorem is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository claims linear independence of 1, ζ(2), ζ(3), extending the prior Li₂(1/2) method. Agents formalized the polynomial construction and estimates, while the author also developed the argument; their respective central ideas are not separated.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Moh-curve theorem appears in the author’s manuscript. ChatGPT and Codex assisted mathematical exploration and Aristotle built the Lean proof, but the disclosure does not identify a central original AI proof idea beyond that manuscript.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Black–Scholes pricing and the Girsanov route are established mathematics cited as sources. Agents built the stochastic-calculus Lean library and formal proof, with no new mathematical theorem or method claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The matching and Galton–Watson classification theorems come from Athreya and Troscheit’s paper. The agents wrote and repaired its Lean formalization while the authors designed and reviewed the mathematical statements.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The unconstrained productive-core result addresses a stated open complexity case, but the preserved disclosure names AI only for migration, metadata, and statement packaging. Mathematical discovery provenance remains unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The unistationarity theorem extends an open case in Nandan, Nghe and Unterberger, and Codex assisted development and packaging. The disclosure does not say who supplied the passive-chain, ratio or boundary-Jacobian argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The project records a finite P6 theorem and substantial AI assistance across research, but does not isolate who found its central argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Glazer states that he designed the tower theory, solidity proof, calculus and registered statement. Claude wrote the Lean development and encoding under his direction; no AI-origin mathematical idea is claimed.
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.
