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 27 of 39
The paper reports improved sum–difference exponents and credits Aristotle and GPT models with research and proof derivation. The disclosure does not identify a retained central inequality or transfer step first supplied by AI, so AI origin remains unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository states a new explicit D-stability criterion, but its visible claim evidence does not say who supplied the critical-point construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The coNP-hardness reduction is a new paper result and Codex assisted proof development, but the disclosure does not state whether Mislan or AI devised the integer-matrix/Pell construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The theorem and local-divisor proof come from Krohn–Rhodes and Diekert–Kufleitner–Steinberg. Claude wrote the Lean proof under Rao’s direction; the stated variants are formalization scope, not an AI-origin mathematical contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
AI agents formalized and repaired a proof of Frankl, Kupavskii and Swanepoel’s earlier theorem; the source does not identify a distinct central AI-origin mathematical result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The near-linear cycle theorem is the prior Bucic paper’s result. Aristotle is identified as a Lean editor and Codex as auditing and porting the formalization; neither is credited with the central graph theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This is mainly an AI-written formalization of Hong–Kung, but it also repairs false literal model assumptions and proof steps. The author specifies the corrections; it is unclear whether an AI-origin mathematical correction remains.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository presents a new Li₂(1/2) irrationality proof, but says the agents formalized the polynomial construction under Qian Tang’s direction. It does not identify who devised the construction or key estimates.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The result is the established three-dimensional kissing number 12, following Musin's Delsarte approach. The AI agent wrote the Lean proofs, certificates and preprint under the author's objectives, but no new central mathematical result or proof idea is claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry reports new ACR counterexamples and a block-order completeness result. Its metadata documents AI-assisted migration and preparation but does not identify who devised the networks or completeness proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Adamczewski–Bugeaud result and its Subspace-Theorem machinery are classical published mathematics. The disclosure says agents formalized those fixed targets from Bombieri–Gubler and related sources under Stephan's direction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The claimed attracting periodic orbits answer Vassena’s open question, but cited metadata describes Codex source migration and statement packaging. It does not establish an AI-originated central mathematical argument in Mislan’s companion manuscript.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The record states a new determinant theorem and counterexamples, but the disclosed Codex role is source migration, metadata and packaging. Historical AI development is mentioned without identifying who found the core constructions.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source credits Prusina with the central Gaussian reduction idea. It does not document a retained central gadget or square-reduction idea originated by GPT-6.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected classification is an established human conjecture proved with Vampire. Claude’s documented role is transcription and workflow support.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source does not account for Shahab’s earlier C7 proof and Lean formalization; the chronology and overlap between the constructions remain unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The result and proof are Shelah’s 1975 answer to Erdős Problem 1219. This project formalizes that proof under Ji Ho Bae’s direction; no AI-origin mathematical contribution is disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
A new rooted-interval characterization is claimed, but accessible metadata documents Codex source migration and packaging only; the companion paper PDF’s original AI disclosure could not be resolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The entry formalizes Tao’s 2015 Erdős discrepancy theorem and its cited human proof architecture. It does not identify new central AI mathematical work.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The repository’s paper correspondence maps its adversary and polynomial-method results to prior research. Claude and Codex are credited with development of the Lean library, not with a new query-complexity result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The classification is conditional on five explicit literature assumptions and formalizes Ishiki's paper. Codex handled Lean implementation and alignment, without a documented role in the original classification argument.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The disclosure expressly says this formalizes the published Furber–Mardare–Panangaden–Scott paper and makes no claim that its mathematics originated in the repository. Multiple models assisted with Lean work.
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, leaving both the local-class-field-theory scope and original AI disclosure unaudited.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited global class field theory repository returned no readable snapshot. The title does not establish whether it is only a formalization or contains an AI-origin contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Claude ported Gonthier’s established Coq formal proof of the Four Color Theorem into Lean. The stated AI work is a formalization port of known human mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
The record does not attribute a specific central lower-bound idea to GPT-5.6 Sol rather than the human-directed proof process; an AI-involvement rating would be conjectural.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The RAF abundance equivalence and two partial cases are presented as new, but the AI disclosure covers source migration and packaging without attributing the mathematical ideas.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Main Theorem, Theorems 1–2 and lemmas are assigned to Corvaja–Zannier's 2004 paper; even the stronger Lemma 4 conclusion is described as following from that paper's proof. The releaser chose the paper and scope, Claude performed the formalization, and metadata says all proved mathematics is in print.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript preceded this Lean development, but the disclosure does not resolve who supplied its improved 2/15-scale mathematical argument. Codex agents are credited with proof construction and audits; central AI origin needs clarification.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The repository formalizes published TSP bounds but also exports a strictly larger saving than Song’s stated constant. Its README credits AI-assisted proof development without identifying who found that improvement or whether it is a distinct mathematical advance.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript discloses an initial ChatGPT proof outline for the exponent-three model-companion result, followed by human reconstruction and checking. It is unclear whether a central AI idea survived.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Claude autonomously formalized the source draft, and the disclosure says GPT-6 Pro prepared that draft with significant author input and unpublished human manuscripts. The central theorem and proof ideas cannot yet be apportioned between AI and human sources.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The compared impossibility theorem is attributed to Myerson and Satterthwaite. The disclosure explicitly limits gpt-6-luna to proof engineering of that earlier theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The non-provability result is attributed to Shelah and Stanley’s 1987 forcing argument. Bae supplied the literature connection, mathematical direction, and formalization strategy; agents assisted Lean development of that existing result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected Gibbard–Satterthwaite theorem is established; the source credits AI only with Lean proof engineering of a reduction through Arrow’s theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The manuscript claims new autocatalytic-network criteria and enumeration, while the disclosure identifies AI-assisted development and packaging without tracing central mathematical ideas.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The same-ground RAF characterization and four-reaction threshold are new claims. The cited disclosure identifies Codex migration and packaging but says historical production provenance was not reconstructed, leaving the origin of the central argument unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The finite Arrow theorem and decisive-coalition argument are classical. The project calls itself a reusable formalization with no new mathematics and credits gpt-6-luna with proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source follows Bombieri–Gubler and Schmidt for Roth and Subspace Theorem results. Agents built the Lean libraries from human-directed roadmaps; no new central theorem is attributed to them.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The selected theorems appear to answer sparse-polymer questions, but the Palomar metadata records only Codex-assisted migration and packaging and points to preserved manuscript disclosures. It does not establish who discovered the probability bounds.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The registered theorem is a new constructive attainment result, but the disclosure records only Codex source migration and packaging; historical tool and idea provenance is explicitly unreconstructed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The positive-degradation unistationarity claim may be new, but the cited metadata documents only Codex migration and packaging; the original paper PDF and production history remain unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The irrationality proof is credited to Fauzan’s preprint. Astra and Codex are credited with its Lean formalization and packaging, not the original mathematical proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source presents a new minus-one valuation formula and reports extensive AI-assisted mathematical research, but credits the human maintainer with target and scope decisions without identifying who found the mixed-parity or exceptional-case mechanism.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This formalizes the prior Armstrong–Kuusi–Loher homogenization paper. Agents built and reviewed Lean proofs against author-approved statements, with no distinct AI-origin mathematical idea disclosed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Scott’s 1964 representation theorems are earlier work, while the project separately claims a new infinite Kelley-style characterization. Agents drafted and proved Lean material, but the source assigns the route and review to Ericson without identifying the origin of that new theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The sunflower bounds are credited to ALWZ, Rao and BCW. The repository describes AI-assisted formalization of those published results, not an AI-origin bound.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The four-axiom bargaining characterization is Nash's 1950 theorem. The source calls this a reusable formalization without new mathematics and describes AI as proof engineering.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited repository does not expose a root formalization.yaml. A counterexample title alone cannot establish its origin or the AI role.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The nonnegativity cutoff argument is credited to Jenkins’s source paper. Codex performed Lean development and proof repair under Jenkins’s mathematical direction; no distinct central AI mathematical idea is disclosed.
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.
