Back to Problems

erdos_707.counterexample_hall

Specification

This conjecture was actually first disproved by Hall in 1947 [Ha47], long before Erdős asked this question. A counterexample for any modulus from from [Ha47] in the paragraph following Theorem 4.3, where it was given as $\{-8, -6, 0, 1, 4\}$, but this can be shifted to natural numbers as pointed out in [arxiv/2510.19804].

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem erdos_707.counterexample_hall (A : Set ℕ) (hA : A = {1, 3, 9, 10, 13}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (n : ℕ), A ⊆ B → ¬IsPerfectDifferenceSet B n
ID: ErdosProblems__707__erdos_707.counterexample_hall
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.