Erdős-Sárközy Conjecture Formalization Status

This project aims to formalize the proof of the Erdős-Sárközy conjecture in Lean 4, following the paper "On a problem of Erdős and Sárközy about sequences with no term dividing the sum of two larger terms" by Benjamin Bedert.

Current State

• Completed: Project setup with Lean 4 and mathlib dependency.
• Completed: Formal definition of PropertyP: "no term divides the sum of two larger terms".
• Completed: Formal statement of Bedert's Theorem 1 (Bound: |A| ≤ n/3 + C).
• Completed: Formal statement of Bedert's Theorem 2 (Bound: |A| ≤ ⌊n/3⌋ + 1 for large n).
• Completed: Lemma 1 (Parts 1 & 3): Fully implemented and verified proofs establishing disjointness properties (e.g., A disjoint from k*A).
• In Progress: bedert_lemma_2 structure defined, pending arithmetic bound proofs.

Future Work Required

To fully formalize the entire proof, the following steps are needed:

• Lemma 2 Proof: Complete the arithmetic bounds required for the proof of Lemma 2.
• Lemmas 3-12: Formalize and prove the remaining lemmas from the paper. these involve:
  • Sumset density arguments (e.g., |S+S| bounds).
  • Handling specific modular cases (mod 3, mod 4, mod 12).
  • Constructing auxiliary sets (B1, B2, etc.) to bound the size of A.
• Theorem 2 Proof: Implement the induction argument on n that utilizes the above lemmas to prove the upper bound.
• Theorem 1 Proof: Derive Theorem 1 from Theorem 2 (requires choosing constant C).
• Original Conjecture: Link the formalized Theorem 2 to the original statement of the conjecture.