{
  "abstract": "We resolve a $1,000 Erdős prize problem, complete with formal verification generated by a large language model. In over a dozen papers, beginning in 1976 and spanning two decades, Paul Erdős repeatedly posed one of his \"favorite\" conjectures: every finite Sidon set can be extended to a finite perfect difference set. We establish that {1, 2, 4, 8, 13} is a counterexample to this conjecture. During the preparation of this paper, we found that although this problem was presumed to be open for half a century, Marshall Hall, Jr. published a different counterexample three decades before Erdős first posed the problem. With a healthy skepticism of this apparent oversight, and out of an abundance of caution, we used ChatGPT to vibe prove both Hall's and our counterexamples in Lean.",
  "abstract_shown": true,
  "affiliations": [
    "Independent Researcher",
    "Department of Mathematics, The Ohio State University",
    "Translational Data Analytics Institute, The Ohio State University"
  ],
  "article_type": null,
  "arxiv": null,
  "author_total": 2,
  "authors": [
    {
      "affs": [
        0
      ],
      "name": "Boris Alexeev",
      "orcid": "0009-0002-5290-1735"
    },
    {
      "affs": [
        1,
        2
      ],
      "name": "Dustin G. Mixon",
      "orcid": "0000-0003-2743-7010"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/13mqq0mavnwjs.bib",
  "cited_by": 11,
  "doi": "10.1073/pnas.2531760123",
  "fulltext_url": null,
  "id": "13mqq0mavnwjs",
  "issns": [
    "0027-8424",
    "1091-6490"
  ],
  "landing_url": "https://doi.org/10.1073/pnas.2531760123",
  "language": "en",
  "licence": "CC-BY-NC-ND",
  "licence_label": "CC BY-NC-ND",
  "licence_source": "journal",
  "licence_url": "https://creativecommons.org/licenses/by-nc-nd/4.0/",
  "metadata_licence": null,
  "native_subjects": [
    [
      "openalex",
      "2607|Limits and Structures in Graph Theory"
    ]
  ],
  "openalex": "W4416248783",
  "pdf_url": null,
  "pmcid": "PMC13213966",
  "pmid": "42172271",
  "published": "2026-05-22",
  "publisher": "National Academy of Sciences",
  "ris": "https://research.draconitic.com/paper/13mqq0mavnwjs.ris",
  "sources": [
    {
      "first_seen": "2026-11-07T13:20:42Z",
      "native_id": "W4416248783",
      "source": "openalex",
      "url": "https://doi.org/10.1073/pnas.2531760123"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "openalex:2607|Limits and Structures in Graph Theory",
      "subfield": "combinatorics"
    }
  ],
  "title": "Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof",
  "title_text": "Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof",
  "type": "peer-reviewed",
  "updated_at": "2026-11-07T13:20:42Z",
  "url": "https://research.draconitic.com/paper/13mqq0mavnwjs",
  "venue": "Proceedings of the National Academy of Sciences",
  "versions": []
}