Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof.

Area of Science:

• Combinatorial Number Theory
• Discrete Mathematics
• Set Theory

Background:

• Paul Erdős posed a conjecture in 1976 regarding finite Sidon sets and perfect difference sets.
• The conjecture remained open for decades, becoming a notable problem in combinatorial mathematics.

Purpose of the Study:

• To resolve the Erdős conjecture on extending finite Sidon sets to finite perfect difference sets.
• To provide a counterexample to this long-standing mathematical problem.

Main Methods:

• Identification of a specific finite set {1, 2, 4, 8, 13} as a counterexample.
• Formal verification of the counterexample using a large language model (ChatGPT) within the Lean theorem prover.
• Discovery of a prior counterexample by Marshall Hall, Jr.

Main Results:

• The Erdős conjecture is disproven.
• The set {1, 2, 4, 8, 13} serves as a concrete counterexample.
• Marshall Hall, Jr. had previously published a different counterexample, predating Erdős's conjecture.

Conclusions:

• The problem of extending finite Sidon sets to finite perfect difference sets is definitively closed.
• Large language models can assist in formal verification of mathematical proofs.
• Historical mathematical literature may contain overlooked solutions to prominent problems.