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 32 of 39
The original Paper C manuscript reports substantial model help with lemma exploration and proof development. Six external literature propositions remain explicit premises; the disclosure does not isolate which retained central lemma came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Friendship Theorem is credited to Erdős–Rényi–Sós and Wilf. The disclosed Gemini agent workflow formalized this established theorem under maintainer direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry formalizes the classical Erdős–Ko–Rado theorem and Hilton–Milner construction. Its disclosure describes agentic Lean proof work under maintainer direction, with no AI-origin central mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Bollobás’s 1965 Two Families Theorem is the stated source. Gemini agents formalized and checked it in Lean; the disclosure does not claim a new AI-origin mathematical theorem or proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry formalizes Bondy's 1972 induced-subsets theorem. Gemini agents are credited with Lean proof development under maintainer direction, not the theorem or a new central proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited version appears to select the noncube (6,9) two-sheet/valuation result within a multi-target repository. The source report precedes Codex’s Lean translation, but its mathematical producer and any AI-originated valuation insight are unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Graham–Pollak and Tverberg supply the theorem and linear-algebra proof. Gemini agents implemented and checked the Lean formalization under maintainer direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source-admissible variational closure uses laboratory-specified statements and Aristotle/Claude proof work. The disclosure does not identify AI as supplying the central analytic idea rather than proving specified subgoals.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The six selected claims are attributed to Dana Scott's 1976 paper. The original disclosure says AI agents wrote Lean formalization and proof engineering under Ericson's direction and review; it does not credit them with new central mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The named order isomorphisms independently prove a known Scott/folklore equivalence. Grok developed Lean bridges, while Ericson chose and reviewed the route; the source says the equivalence is not original.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The underlying manuscript is unavailable in the cited source, preventing a comparison of Theorem 1.1 and its proof with the Lean statement.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Scott’s Theorem 8.8 is the sourced result. Cursor, Claude and GPT agents formalized, repaired and packaged it under a human-chosen route; no new AI mathematical contribution is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Huang's new shifted-theta completion and its formalization were developed together. Agents proposed proof steps under human direction, but the public disclosure does not identify whether an AI supplied the central row factorization or completion.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The assessed theorem is Dana Scott’s 1972 Theorem 4.4 with Milner’s correction. Agents formalized the existing argument; the author chose the route and reviewed definitions.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository first presents an explicit sofic non-MF group and lists GPT and Claude agents, but records no division of mathematical labor. Central AI origin cannot be inferred from model names alone.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared claim is the first sentence of Scott's 1982 Theorem 7.2. Agents wrote the Lean, including heavy proofs; Ericson chose the route and reviewed the claims. No distinct AI domain-theory idea is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited Euclidean Jordan repository could not be retrieved, so the original statement, proof origin and AI disclosure cannot be checked. The two registry records share one exact cited repository and remain separate entries. This decision concerns 000006 specifically.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited Euclidean Jordan repository could not be retrieved, so the original statement, proof origin and AI disclosure cannot be checked. The two registry records share one exact cited repository and remain separate entries. This decision concerns 000005 specifically.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository does not expose a root formalization.yaml, so no original theorem or AI/proof disclosure was available to audit.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The q-series paper and Lean formalization were developed together with AI proof development and model audits. The disclosure does not identify who found the prime-index classification or decisive invariant.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper is described as human-written and author-verified, but GPT-5.5 Pro was used in initial proofs and the disclosure does not clarify whether it supplied a central rank-parity idea or only proof assistance.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Kinnim optimization theorem follows Koppel’s interpretation and Reiss’s published proof. Agents strengthened the Lean encoding to physical ownership worlds but no independent AI mathematical result is documented.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited sequential-products repository could not be read through GitHub or the source browser, so its claim and original AI/proof disclosure remain unverified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This second cited revision again lists several original manuscripts, while the registry entry cannot be matched to one selected project from the accessible repository index. Its original disclosure needs project-level review.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited collection contains six separate paper and Lean packages, but the queue gives two generic titles without project paths. Their disclosures vary, including AI assistance with mathematical derivation, so neither entry can be excluded or advanced without mapping its registry claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Huang claims a new signed Hahn-branch coefficient argument for the Hickerson–Mortenson identity. Agents proposed proof steps, but the record does not say whether they originated the central new argument or only helped formalize a human manuscript.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited collection contains six separate paper and Lean packages, but the queue gives two generic titles without project paths. Their disclosures vary, including AI assistance with mathematical derivation, so neither entry can be excluded or advanced without mapping its registry claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The public source does not show how much of GPT Pro’s proposed analytic proof survived later reconstruction and repair.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited README distinguishes a registered Fredholm strong-closure theorem from a separate unproved zero-density candidate. It describes verification and an agentic laboratory but does not establish who supplied the registered theorem’s central endpoint-tapered construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited sequential-products repository could not be read through GitHub or the source browser, so its claim and original AI/proof disclosure remain unverified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This wrapper says the proof was mostly written and reviewed by humans, but its acknowledgements credit Claude Fable 5, with Akhil Mathew, in the original counterexample announcement. The exact AI-origin role in the counterexample is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository lists several original manuscripts and Lean projects, but the inaccessible registry record does not identify which project this entry selects; its AI/proof disclosure cannot be safely matched.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository presents a candidate zeta-zero improvement and distinguishes measured, cited and unclosed steps, but its root disclosure does not identify the origin of the proposed mathematical step or a completed global theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The fixed repository README only indexes six paper-specific Lean projects. It does not identify which Palomar entry is assigned here or disclose AI’s role in that particular mathematical claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited sequential-products repository and its original AI/proof disclosure could not be read. The registry title alone cannot establish a claim or central AI origin.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author supplied an unpublished manuscript and its proofs for three probabilistic extrapolation theorems. Claude wrote the Lean implementation from those proofs and discussed the problem, with no central AI-origin result identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not identify a central AI-origin lemma or proof step retained in the Poisson theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The comparator states the Fu–Qin–Wang spectral-gap theorem. Codex prepared the standalone challenge and solution bridge under human prompts; no new mathematical result is claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The basis-count identity is presented as original work and its write-up and formalization were produced by AI agents. The author selected and reviewed the claims, while the record does not identify who conceived the identity or its asymptotic argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Landau identity, Tsirelson norm bound and real-Pauli attainment follow cited earlier work. Alexander fixed and reviewed statements; Claude drafted Lean. The real C*-algebra scope and scalar-square counterexample do not carry separate AI-origin attribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The rank-two no-spurious-critical-points theorem is Legat–Yuan–Parrilo’s 2023 result. GPT-5.4 is disclosed as a directed Lean coding agent, with the human formalizer checking the statement against the paper.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source says this proof descends from Mazur’s earlier AI-assisted Sendov proof through Tao’s digestion and expressly claims no new mathematics. Claude wrote Lean proofs and certificate machinery under Tao’s plans; the equality case is also an earlier result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The characteristic-zero ODE rigidity theorem follows a human campaign proof supplied in the prompt. A positive-characteristic strengthening was extracted from that proof, but the source does not establish who devised this separate extension.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The factor-language chirality argument differs from cited tiling-space work. The author fixed statements while Claude drafted proofs; the record does not say who supplied the successor-invariant or palindrome-window ideas.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Theorem A follows a supplied campaign proof, but Claude designed the standalone positive-characteristic statement extracted from its remark. The centrality and originality of that extracted strengthening are unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Wallace counterexample is in Fraga and Rodrigues’s source paper. Codex generated the entire Lean development, while the authors supplied mathematical objectives, context and ideas; the source does not resolve whether AI supplied a central part of the original construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository formalizes Pick’s theorem, the Jordan curve theorem, and Radó’s theorem, all established results. Autonomous agents developed Lean proofs under high-level human direction; the source does not claim a new mathematical theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The lower-bound theorem is first presented in the author’s working draft; the disclosure says human mathematical direction with AI-assisted proof engineering, without assigning the central collision-lattice argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The prime-gap bound of 246 is an established conditional result being formalized. The disclosure credits AxiomProver with autonomous theorem formalization, while no new mathematical bound or idea is identified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The corrected low-individual-degree-test theorem follows Ji–Natarajan–Vidick–Wright–Yuen. Its k ≥ 400md and k > 0 conditions are disclosed; authors chose and checked the statement, while agents wrote Lean.
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.
