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 15 of 39
The linked Erdős #130 page could not be read here, and this assignment supplies no original proof or AI-origin account. Its problem statement and any model contribution remain unestablished.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The authors say model use was limited to brainstorming, discussing possible approaches and preliminary checking; they independently wrote the mathematical arguments and identify no retained central AI idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The authors disclose Codex assistance with readability, selected calculations, exploration of the s=3 case and reorganization of a lemma, but do not identify a retained central AI-origin result for the bounded-circumference cycle count.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author credits ChatGPT with the initial proof framework of Lemma 2, an auxiliary approximation lemma. Whether this supplied a central idea for the Tokuda lower bound is unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
Different claim: a counterexample for non-convex windows, not the rectangular-window Nivat proof. Keep pending for separate claim review.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18
Kintali’s cycle-double-cover manuscript claims a proof, and a separate OpenAI Lean repository discusses formalization, but the manuscript does not document a central AI contribution. The relation between these artifacts and the claimed proof remains unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The authors credit ChatGPT with programs used for symbolic computation in the counterexample search. The disclosure does not say whether those programs found the retained configuration or merely checked a human candidate.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The accessible original comment gives an analytic counterexample but no specific AI provenance for its construction or proof.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The original toric-Fano preprint was readable, but it did not identify a central AI contribution; absence of a disclosure is insufficient to exclude the registry claim. The registry page itself was inaccessible.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This listing describes the same theorem as the signed-bar record, whose central AI attribution remains unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author reports GPT-5.6 Sol helped explore the subdivision scale, but does not specify whether it found the retained central construction or only aided parameter choice.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source describes extensive model assistance but does not isolate a retained model-origin central proof step in the final theorem.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The linked problem record was not readable here, and several distinct proposed resolutions appear in the source trail; the exact AI-origin claim represented by this entry is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The secondary record credits GPT-5.6 Sol with a bound, but the original Erdős problem record could not be read to confirm the statement and attribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The cited Erdős problem page was unavailable, leaving the claimed solution and AI origin unverified from the original source.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The registry attributes a solution to GPT-5.6, but its only linked original problem record was unreadable and no original proof or provenance disclosure was located.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The original Erdős #320 page could not be read. A secondary index says GPT-5.6 Sol supplied a matching upper bound, but no first-person proof or disclosure was available to establish the precise contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The community entry claims GPT-5.6 Sol proved an asymptotic formula for F(n) and that Lean checked it; the original #793 record was inaccessible, leaving the exact theorem, proof and provenance unconfirmed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The decisive construction arose in discussions with ChatGPT, but the source does not identify whether the model or author proposed it.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-19T00:00:00.000Z
The authors credit ChatGPT with assistance developing CP-SAT models, then report independent checks; the disclosure does not say whether AI originated a central search formulation or only implemented human specifications.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The accessible short paper discusses a finite-automata Bernoulli-factory claim but gives no clear first-person account assigning a central mathematical contribution to AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author says the research direction and ideas were human-origin, while models developed technical lemmas and calculations; the disclosure does not isolate a retained central AI result.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The authors disclose AI use for editing and software; Codex unexpectedly enumerated an LP face, which influenced direction, but explicitly state they conceived and verified all mathematical results and arguments.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author reports extensive GPT-5.5 Pro interaction, but says its suggestions were substantially revised and corrected; the source does not identify a retained central AI construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper explicitly says GPT-5.5 auto-formalized the authors’ main Theorem 1.2; it attributes no new mathematical construction or proof idea to AI. Formalizing an existing human result alone fails the curation threshold.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The linked Problem 1061 record was not readable, and this entry does not identify which proof or model contribution it represents.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author says ChatGPT substantially developed technical lemmas and calculations, while the research directions and ideas were human-originated; the central retained AI part of the sum-of-divisors proof is unspecified.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The original paper and repository document an extensive Aristotle-assisted Lean development, but do not identify whether AI originated the classification and exact-spectrum ideas rather than formalizing supplied human mathematics.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This listing describes the same Erdős 768 result; the model’s central mathematical role remains unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-19T00:00:00.000Z
The source does not identify the central mathematical step supplied by ChatGPT, so the AI contribution cannot yet be assessed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The acknowledgments credit GPT-based tools with proposing strategies and auxiliary lemmas and helping formalize selected components, yet do not isolate a retained central AI idea for the anti-Bertini construction.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author describes ChatGPT as a sounding board for organizing optimization and checking cutoff calculations, with other models used for editing; no model-origin restriction construction or theorem is claimed.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The linked Overleaf manuscript was inaccessible, and the Erdős #671 problem page did not expose a proof or first-person AI origin account. The claimed result and model contribution cannot yet be distinguished.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author says humans originated the ideas and research directions while models developed technical lemmas, calculations and Lean code; the retained central AI contribution to Erdős #550 is unclear.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The determinant paper presents a proof of Sun’s conjecture but the available original HTML gives no division of mathematical work with AI; the directory label alone cannot establish central AI origin.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The source reports model assistance with a computation and comment but does not identify a retained model-origin bound or proof step.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-19T00:00:00.000Z
The secondary listing credits Aristotle and GPT, but the original Erdős #948 proof record was inaccessible and the model’s actual role is unresolved.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Lean project proves only a limit-exists interpretation; it discloses Codex/ChatGPT assistance with formalization and writing, without isolating an AI-origin proof idea.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The directory attributes the #1197 disproof to Aristotle, Claude and GPT and reports Lean verification, but links only the inaccessible problem record; no first-person proof provenance was available here.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The queued original Erdős problem page returned 403, so the claimed solution and AI provenance could not be checked.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The author reports GPT-assisted strategy and lemma suggestions plus Lean formalization of selected components, but does not identify which central obstruction, if any, originated with AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The Erdős problem page was blocked, and the paired arXiv paper needs direct review before this broad problem entry can be tied to a specific AI contribution.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper credits ChatGPT with broad ideation, proof exploration and programming for a shifted pairwise-coprime average-order theorem, but does not identify a retained central theorem idea attributable to it.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
This listing does not establish a separate AI-origin result in Bradač’s earlier construction; the later model-attributed sharp exponent is a distinct claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The original abstract proves the conjecture only in a polynomial chromatic-sparsity regime. The accessible original record does not document which, if any, central proof step came from AI.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The algebraic C*-algebra result is attributed to Akbas and Sra; the accessible manuscript has not established a retained AI-originated central step for this stronger claim.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The problem discussion links a short paper and Lean theorem for a kappa-equals-2 case but does not establish that AI originated central mathematical work or that this scope resolves all of Erdős 942.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper proves the circle-minimizer statement but describes ChatGPT help with conceptualization and computations without identifying a central model-origin mathematical step.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The listed Google Drive note could not be read here, so neither the exact Erdős 326 claim nor central AI origin is established.
Screening recorded: 2026-10-17 · Decision reviewed: 2026-10-18T00:00:00.000Z
The paper’s Use of AI credits assistants with Lean formalization, Python scripts and exposition while the author directed the mathematics and adapted a prior human induction method; it does not credit AI with the semiprime proof idea.
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.
