Formalizing a proof (the prime case of) Erdos problem #707 recently proven by Alexeev, ChatGPT, Lean, and Mixon at https://borisalexeev.com/papers/erdos707.html, following Theorem 8 proven on page 5

def IsPerfectDifferenceSet {N : ℕ} (B : Finset (ZMod N)) : Prop

A perfect difference set is a set where every nonzero element is uniquely representable as a difference of two elements of the set.

Equations

• IsPerfectDifferenceSet B = ∀ (d : ZMod N), d ≠ 0 → ∃! b : { x : ZMod N // x ∈ B } × { x : ZMod N // x ∈ B }, ↑b.1 - ↑b.2 = d

def IsPerfectDifferenceSet.map {N : ℕ} (B : Finset (ZMod N)) (p : { x : ZMod N // x ∈ B } × { x : ZMod N // x ∈ B } ⊕ Unit) : ZMod N ⊕ { x : ZMod N // x ∈ B }

Equations

• IsPerfectDifferenceSet.map B (Sum.inl p_2) = if p_2.1 = p_2.2 then Sum.inr p_2.1 else Sum.inl (↑p_2.1 - ↑p_2.2)
• IsPerfectDifferenceSet.map B (Sum.inr val) = Sum.inl 0

theorem IsPerfectDifferenceSet.card {N : ℕ} [NeZero N] {B : Finset (ZMod N)} (hdiff : IsPerfectDifferenceSet B) : B.card * B.card + 1 = N + B.card

class Mainstep.Hypotheses : Type

We will show that the following hypotheses are inconsistent; this is the bulk of the proof of Theorem 8.

• p : ℕ
• hp : Nat.Prime p
• N : ℕ
• hN : N = p ^ 2 + p + 1
• B : Finset (ZMod N)
• hdiff : IsPerfectDifferenceSet B
• embed : { x : ℕ // x ∈ {1, 2, 4, 8} } → { x : ZMod N // x ∈ B }
• h_embed (n : { x : ℕ // x ∈ {1, 2, 4, 8} }) : ↑(embed n) = ↑↑n
• h_inj : Function.Injective embed

theorem Mainstep.h1 [Hypotheses] : 1 ∈ B

theorem Mainstep.h2 [Hypotheses] : 2 ∈ B

theorem Mainstep.h4 [Hypotheses] : 4 ∈ B

theorem Mainstep.h8 [Hypotheses] : 8 ∈ B

theorem Mainstep.h2_ne_1 [Hypotheses] : 2 ≠ 1

theorem Mainstep.h4_ne_1 [Hypotheses] : 4 ≠ 1

theorem Mainstep.h4_ne_8 [Hypotheses] : 4 ≠ 8

theorem Mainstep.hodd [Hypotheses] : Odd N

theorem Mainstep.card_B [Hypotheses] : B.card = p + 1

theorem Mainstep.odd_P [Hypotheses] : Odd p

theorem Mainstep.heven [Hypotheses] : Even B.card

theorem Mainstep.mul_two_inj [Hypotheses] {x y : ZMod N} (h : 2 * x = 2 * y) : x = y

theorem Mainstep.diff_uniq [Hypotheses] {a b c d : { x : ZMod N // x ∈ B }} (ha : a ≠ b) (hsub : ↑a - ↑b = ↑c - ↑d) : a = c ∧ b = d

noncomputable def Mainstep.f [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b : { x : ZMod N // x ∈ B }) : { x : ZMod N // x ∈ B }

Given a perfect difference set B and an element a not in B, the function f_a maps each b ∈ B to the unique c ∈ B such that a-b=c-d for some d ∈ B.

Equations

• Mainstep.f ha b = (Exists.choose ⋯).1

noncomputable def Mainstep.g [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b : { x : ZMod N // x ∈ B }) : { x : ZMod N // x ∈ B }

Though not defined in Theorem 8, it is convenient to also introduce the companion function g_a, defined to be the d element.

Equations

• Mainstep.g ha b = (Exists.choose ⋯).2

theorem Mainstep.f_def [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b : { x : ZMod N // x ∈ B }) : a - ↑b = ↑(f ha b) - ↑(g ha b)

theorem Mainstep.f_def' [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b c d : { x : ZMod N // x ∈ B }) : a - ↑b = ↑c - ↑d ↔ c = f ha b ∧ d = g ha b

theorem Mainstep.f_inv [Hypotheses] {a : ZMod N} (ha : a ∉ B) : Function.Involutive (f ha)

f_a is an involution.

theorem Mainstep.f_fixed [Hypotheses] {a : ZMod N} {ha : a ∉ B} {b : { x : ZMod N // x ∈ B }} (hb : f ha b = b) : 2 * ↑b = a + ↑(g ha b)

Fixed points of f_a satisfy 2f_a(b) = a + g_a(b).

noncomputable def Mainstep.z2_vact [Hypotheses] {a : ZMod N} (ha : a ∉ B) : AddAction (ZMod 2) { x : ZMod N // x ∈ B }

Equations

• Mainstep.z2_vact ha = { vadd := fun (i : ZMod 2) (b : { x : ZMod Mainstep.N // x ∈ Mainstep.B }) => if i = 1 then Mainstep.f ha b else b, zero_vadd := ⋯, add_vadd := ⋯ }

theorem Mainstep.f_second_fixed [Hypotheses] {a : ZMod N} {ha : a ∉ B} {b : { x : ZMod N // x ∈ B }} (hb : f ha b = b) : ∃ (c : { x : ZMod N // x ∈ B }), c ≠ b ∧ f ha c = c

If there is one fixed point, there is another.

theorem Mainstep.two_mul_sub_one_notin [Hypotheses] {x : { x : ZMod N // x ∈ B }} (hx : ↑x ≠ 2) : 2 * (↑x - 1) ∉ B

theorem Mainstep.first_fixed [Hypotheses] {x : { x : ZMod N // x ∈ B }} (hx : ↑x ≠ 2) : f ⋯ x = x

theorem Mainstep.second_fixed [Hypotheses] {x : { x : ZMod N // x ∈ B }} (hx : ↑x ≠ 2) : ∃ (b : { x : ZMod N // x ∈ B }), b ≠ x ∧ f ⋯ b = b

noncomputable def Mainstep.b [Hypotheses] (x : { x : ZMod N // x ∈ B }) : { x : ZMod N // x ∈ B }

Equations

• Mainstep.b x = if hx : ↑x = 2 then ⟨2, ⋯⟩ else ⋯.choose

noncomputable def Mainstep.d [Hypotheses] (x : { x : ZMod N // x ∈ B }) : { x : ZMod N // x ∈ B }

Equations

• Mainstep.d x = if hx : ↑x = 2 then ⟨2, ⋯⟩ else Mainstep.g ⋯ ⋯.choose

theorem Mainstep.b_neq [Hypotheses] {x : { x : ZMod N // x ∈ B }} (hx : ↑x ≠ 2) : b x ≠ x

theorem Mainstep.bd_ident [Hypotheses] (x : { x : ZMod N // x ∈ B }) : 2 * ↑(b x) = 2 * (↑x - 1) + ↑(d x)

theorem Mainstep.d_injective [Hypotheses] : Function.Injective d

theorem Mainstep.d_surjective [Hypotheses] : Function.Surjective d

theorem Mainstep.d1_eq_4 [Hypotheses] : d ⟨1, ⋯⟩ = ⟨4, ⋯⟩

theorem Mainstep.d1_eq_8 [Hypotheses] : d ⟨1, ⋯⟩ = ⟨8, ⋯⟩

theorem Mainstep.contradiction [Hypotheses] : False