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 24 of 39
The cited thesis-lean source revision could not be retrieved, so neither the dynamic MCS theorem nor AI provenance was checked.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The theorem statements come from Bárány, Kolossváry, and Troscheit’s paper. The disclosure assigns Claude and GPT-6 to formalization planning, Lean proofs, and correspondence review, while humans designed the statements.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Feldman supplied the mathematical source/interpretation and Claude translated the existing OpenAI argument into Lean. No new central mathematical idea is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README says human investigators directed the mathematical research and made judgments while AxiomProver generated proofs and formalization. The central original proof idea attributable to AI is not specified; inspect the paper/provenance before inclusion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The graph construction is the classical Mycielski/Tutte–Zykov variant. Agents wrote its Lean formalization and explicitly disclaim new mathematical novelty or a solution of Erdős Problem 627.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Parts (i) and (ii) of Erdős 836 are credited to Alon and Price, while the formalization also claims structural bounds on codimension-one avoidance. The AI disclosure gives only general proof-development credit and does not identify the origin or exact novelty of those bounds.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source documents AI exploration and checking but does not identify an AI-origin central 0.74 macro-cluster or Gram-completion construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository could not be read: the root formalization file returned 404 and the cited tree was unavailable. The title alone cannot establish whether the Batson–Spielman–Srivastava formalization contains distinct AI mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The exact metrization equivalence follows Sakai's Theorem 2.3.4 and Lemma 2.3.3. The cited source credits Codex with substantive Lean proof, tests and packaging of that selected classical theorem, with an implementation change from an ℓ¹ to a uniform-metric embedding.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README and formalization metadata explicitly describe formalizing Chen–Hou–Liu’s human mathematical theorem; Codex only assisted migration, extremal-limit extension and verification. No new central AI mathematical contribution is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The disclosure records exploration and Lean assistance without locating the central lower-bound idea or a complete historical division of mathematical credit.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The pinned README explicitly formalizes Hajnal–Szemerédi's 1970 theorem by Kierstead–Kostochka's 2008 human proof. Claude and Aristotle generated Lean code and lemmas, while the human author chose the result and route; no new AI-origin mathematical theorem is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
Both anti-Ramsey formulas were established in cited earlier papers. The agents developed Lean proofs and audits of those known cycle and path results, without a new mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The main perfect-map invariant and regular-space refinement criterion are identified with Munkres and Sakai; the README says the extra Lean API is classical infrastructure and does not claim mathematical novelty. Codex authored implementation and packaging.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The pinned README and formalization metadata say this project formalizes Theorem 1.1 of Vlado Vojdanovski's paper; GPT-6 supplied AI-assisted Lean proof development, with no documented new mathematical contribution beyond that human result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The selected Hilbert-function and syzygy statements are explicitly formalized from the earlier paper’s Theorem 1.1 and Corollary 5.1. GPT-6 agents developed the Lean proofs; no new central mathematical result is attributed to them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The full versioned record and pinned challenge concern a known human theorem, earlier human argument or selected partial formalization. AI transcription, proof completion under a supplied argument or checking alone does not qualify as a new central AI contribution. This decision is about the reviewed formalization, not a refutation of the mathematics.
Screening recorded: 2026-10-22 · Decision reviewed: 2026-10-22T07:39:59.456Z
The pinned README maps 33 formal statements to Fröhlich–Spencer and Kharash–Peled human results. AI coding agents wrote Lean under the authors' supervision; the authors approved exact statements, and no new central AI mathematical theorem is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
Erdős #1180 main affirmative theorem and Glibichuk/Shparlinski bounds are human results. The subproject also proves new-looking staircase bounds and a small-prime correction, but metadata only states AI-assisted proof development; hold until central AI origin and distinct baseline are established.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The pinned README says the project proves Theorem 1.1 and Corollary 1.2 of Hang Lu Su's paper. Codex and Claude substantially developed formal proofs and review reports, but the central even-rank classification is attributed to the human paper.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The selected three-way characterization is expressly Dowker’s 1951 Theorems 2 and 4 and Lemma 3. Codex authored the Lean implementation and review; no new central topology result is credited to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The pinned aging repository formalizes a same-titled paper by P. M. Aronow and Patrick Lopatto. Metadata credits autonomous GPT-6 agents with proofs, mathematical-assumption corrections and proof routes, but does not identify whether the paper's central new aging conclusions originated with AI or the human authors. The manuscript/provenance needs a claim-level attribution review before inclusion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The endpoint is an explicit-cutoff reformulation of a cited human theorem; automation notes say AI assisted implementation, while attribution for any new cutoff argument is unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected conditional lower bound adapts Pollack–Pomerance’s counting argument under the explicit smooth-successor hypothesis. ChatGPT wrote its Lean proof; the AI-linked WD corollary is expressly outside this selected statement.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README presents quantitative reaction-network bounds and source-reported kernel checks, but does not document AI as origin of the new estimates or constructions; inspect manuscript provenance.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The theorem and mathematical manuscript were supplied and revised by Vojdanovski; Codex translated and repaired the Lean implementation.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
Pinned README gives a stable-regime theorem but describes multiple AI-assisted workflows with no reliable finer attribution; current selected 12-claim comparator configuration lacks a public completed run in the pinned snapshot.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The source credits AI with formalization and proof extensions, but attributes the selected theorem and central perturbation idea to the human-authored paper.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This reconstructs the previously solved parts of Erdős 261 and a finite verification: the disclosure names Borwein–Loring and later published bounds as the sources, with AI used for proof development and packaging.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The geometric reduction from point-set lines to pairwise-balanced designs is expressly credited to a human and the quantitative bound to Colbourn–Phelps–Rödl. The LLM assisted Lean proof search and elaboration.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Pinned README gives a new explicit Erdős #206 construction and complete Lean check but credits Yuhang Shi; it does not document AI supplying the construction. Seek provenance before inclusion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The product and Hausdorff-target characterization are Michael's 1968 Theorems 1.2–1.3. Codex supplied Lean and an alternate proof organization, without a separate AI mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The forest-unimodality theorem and subsequent mathematical arguments are credited to Zhang, Li and Vallier manuscripts. AI systems produced the Lean modules and certificates under Vallier’s direction, not the central theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The mathematical source for the bounded holomorphic bases is nonpublic. Codex materially generated the Lean proof, but the disclosure does not distinguish any AI-origin central mathematics from formalizing that source.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The companion shared-resource manuscript claims new criteria and dynamics, while the disclosure groups AI source analysis, proof drafting, manuscript editing, and exact arithmetic together. It does not assign the central new ideas to AI or the human author.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository reports improved zero-density estimates and AI-assisted formalization, but the cited README does not assign the new large-values or density argument to AI or specify the division of mathematical work.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Lean development follows Armstrong–Bou-Rabee–Kuusi’s paper, with agents working on author-specified statements. The paper’s own AI/proof disclosure is needed before excluding the original result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
AI agents formalized and repaired a pre-existing proof, but the source does not isolate a distinct central AI-origin result or proof method.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The fixed-temperature N^(-7/10) SK mean-bias bound is Aronow–Lopatto's manuscript Theorem 1.1 for β > 1 and N ≥ 2. Sol 6.1 autoformalized their development; Codex later prepared interfaces and reviewed it.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript’s authors wrote and revised the coarse-ellipticity results and approved every formal statement. The disclosure assigns models Lean proof development and audits, without documenting an AI-origin central result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected minimax-rate bounds are Theorem 2.3(a,b) of Aronow–Kallus–Lopatto. Sol 6.1 autoformalized the development; Codex supplied interface/compatibility proofs and review, not the original rate claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The mathematical kinetic Aleksandrov estimates are attributed to Loher, Mooney and Mouhot’s source papers. AI agents formalized author-approved statements and proof routes in Lean; the disclosure does not identify a separate AI-origin central result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository reports AI tools in both paper and formalization work and one agent-found improvement, but the selected conditional 1.04315 Lean theorem is tied to Naslund’s main construction. The source does not assign its central mathematical steps to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The new variance-estimation bounds are in a supplied Aronow–Lopatto manuscript. Sol 6.1 autoformalized substantive proofs, but the record does not resolve whether the central statistical idea or revised local-operator lemma originated with AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected replica-symmetry-breaking claims are Lopatto’s paper Theorems 1.1–1.2. Sol 6.1 autoformalized the development and Codex performed compatibility, interface and review work; no new AI mathematical claim is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Mislan’s manuscript claims a new measurable-rate endotactic permanence result using a method from OpenAI’s weakly reversible work. AI proof assistance is disclosed, but the retained new argument’s origin is not allocated.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Hörmander and Rothschild–Stein statements follow named source proofs, but the disclosure says AI models supplied arguments filling gaps in the printed proofs. It does not establish whether those arguments are routine formalization or a central new proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected AT-line statements come from Lopatto’s paper. Sol 6.1 autoformalized and Codex reviewed, ported, and verified the Lean proof; no original AI mathematical idea is documented for these claims.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Vidick and collaborators supplied the manuscript, blueprint and modelling choices; Claude wrote formal proof code for that human mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The PCP, MaxSNP and APX results and their proof routes are attributed to earlier papers and the OpenAI gap-amplification development. Claude agents adapted and formalized those results; no new central result or proof 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.
