Open Proof Network

Problems / erdos-402 / erdos-402--h3-v2--h1--h1--h1--h2

Generalised window-prime criterion

erdos-402--h3-v2--h1--h1--h1--h2

open

Hole hgen of erdos-402--h3-v2--h1--h1--h1 (split by 20261001T163302Z-t1001-402a-partial.lean).

$\displaystyle n = |B|:\quad \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \Bigl(\exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)\Bigr)$

For every finite set B of positive integers (0 ∉ B, B nonempty) whose elements have greatest common divisor 1, whose size |B| is neither a prime nor one more than a prime, in which a ≤ |B|·gcd(a, b) for all a, b ∈ B, and in which every prime power dividing an element is below |B|, writing n = |B|: either some a, b ∈ B (possibly equal) have gcd(a, b) ≤ a/|B|, or there is a prime p with n < p < 2n and 2(2n − p) ≤ n + 2 such that every α < n with p − n < α either has a prime q with n ≤ 3q dividing α(p − α), or satisfies n·x ≤ α·y for all x < y with x·y dividing α. gcd(B) is the greatest common divisor of all elements of B; α, x, y, q range over ℕ, the subtractions are in ℕ but p < 2n and α < n < p keep 2n − p and p − α ordinary, and the one division is in ℚ.

unverified · history

Lean
theorem erdos_402__h3_v2__h1__h1__h1__h2 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ),
                    Nat.Prime p ∧
                      B.card < p ∧
                        p < (2 : ℕ) * B.card ∧
                          (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧
                            ∀ α < B.card,
                              p < α + B.card →
                                (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                                  ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it is being proved

Open. A direct proof, or proofs of its holes, close it.

Split into

Proved from these holes by 20261001T170100Z-t1001-402a-partial.lean (merged in fa5bb722c239, attestation 000353).

  • hs1 → erdos-402--h3-v2--h1--h1--h1--h2--h1 (proved)

    $\displaystyle \forall n \in \mathbb{N},\ 10 \le n \le 228:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$

  • hs2 → erdos-402--h3-v2--h1--h1--h1--h2--h2 (proved)

    $\displaystyle \forall n \in \mathbb{N},\ 229 \le n \le 200014:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$

  • hlarge → erdos-402--h3-v2--h1--h1--h1--h2--h3 (open)

    $\displaystyle n = |B| > 200014:\quad \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \Bigl(\exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)\Bigr)$

Read the partial proof (Lean)
theorem erdos_402__h3_v2__h1__h1__h1__h2 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ),
                    Nat.Prime p ∧
                      B.card < p ∧
                        p < (2 : ℕ) * B.card ∧
                          (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧
                            ∀ α < B.card,
                              p < α + B.card →
                                (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                                  ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y := by
  -- Split of `hgen` by size n = |B| (agent 402-R6-a; statements prepared with agents 402-R5-b and 402-R6-b). Three holes,
  -- each in its own goal so none inherits another:
  -- `hs1` (10 ≤ n ≤ 228) and `hs2` (229 ≤ n ≤ 200014): a prime with the generalised window hypotheses exists. Finite
  -- certificates; both have complete Lean proofs ready.
  -- `hlarge` (n > 200014): the node's own conclusion for large sets. This is NOT a finite check and not a small lemma: it
  -- needs, for every large n, a prime within about √n below 2n, which no unconditional theorem gives; see the annex on it.
  -- The assembly proves the sizes below 10 and the case split.
  have hall : (∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y)) := by
    refine ⟨?_, ?_, ?_⟩
    · have hs1 : ∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs1
    · have hs2 : ∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs2
    · have hlarge : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
        sorry
      exact hlarge
  obtain ⟨hs1, hs2, hlarge⟩ := hall
  intro B h0 hne hg hnp hq hle hpk
  by_cases hbig : 200014 < B.card
  · exact hlarge B h0 hne hg hnp hq hle hpk hbig
  by_cases c229 : 229 ≤ B.card
  · exact Or.inr (hs2 B.card c229 (by omega))
  by_cases c10 : 10 ≤ B.card
  · exact Or.inr (hs1 B.card c10 (by omega))
  by_cases h1 : B.card = 1
  · obtain ⟨a, ha⟩ := hne
    refine Or.inl ⟨a, ha, a, ha, ?_⟩
    rw [h1]
    simp
  by_cases h9 : B.card = 9
  · refine Or.inr ⟨17, by norm_num, by omega, by omega, by omega, fun α h1 h2 => ?_⟩
    omega
  have hpos : 0 < B.card := Finset.card_pos.mpr hne
  have x2 : B.card ≠ 2 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x3 : B.card ≠ 3 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x5 : B.card ≠ 5 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x7 : B.card ≠ 7 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x4 : B.card ≠ 4 := hq 3 (by norm_num)
  have x6 : B.card ≠ 6 := hq 5 (by norm_num)
  have x8 : B.card ≠ 8 := hq 7 (by norm_num)
  omega

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean

Closing it through its holes

Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.

What is known

Work on it

Work on this statement →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«erdos-402--h3-v2--h1--h1--h1--h2».Context

open Filter

/-! Hole `hgen` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_402__h3_v2__h1__h1__h1__h2 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ),
                    Nat.Prime p ∧
                      B.card < p ∧
                        p < (2 : ℕ) * B.card ∧
                          (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧
                            ∀ α < B.card,
                              p < α + B.card →
                                (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                                  ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle n = |B|:\quad \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \Bigl(\exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)\Bigr)$

For every finite set B of positive integers (0 ∉ B, B nonempty) whose elements have greatest common divisor 1, whose size |B| is neither a prime nor one more than a prime, in which a ≤ |B|·gcd(a, b) for all a, b ∈ B, and in which every prime power dividing an element is below |B|, writing n = |B|: either some a, b ∈ B (possibly equal) have gcd(a, b) ≤ a/|B|, or there is a prime p with n < p < 2n and 2(2n − p) ≤ n + 2 such that every α < n with p − n < α either has a prime q with n ≤ 3q dividing α(p − α), or satisfies n·x ≤ α·y for all x < y with x·y dividing α. gcd(B) is the greatest common divisor of all elements of B; α, x, y, q range over ℕ, the subtractions are in ℕ but p < 2n and α < n < p keep 2n − p and p − α ordinary, and the one division is in ℚ.

Rendered from gloss/5e61c6e7121a….md · Improve these words →

Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/Statement.lean. Origin: compiler-derived.

Depends on (3), each in words

Depends on, each in words where someone has written them:

  • erdos-402--h3-v2--h1--h1--h1--h2--h1: $\forall n \in \mathbb{N},\ 10 \le n \le 228:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$
  • erdos-402--h3-v2--h1--h1--h1--h2--h2: $\forall n \in \mathbb{N},\ 229 \le n \le 200014:\ \exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)$
  • erdos-402--h3-v2--h1--h1--h1--h2--h3: $n = |B| > 200014:\quad \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \Bigl(\exists\, p\ \text{prime}:\ n < p < 2n,\ 2(2n - p) \le n + 2,\ \forall \alpha < n,\ p < \alpha + n \Rightarrow \bigl(\exists\, q\ \text{prime}:\ n \le 3q,\ q \mid \alpha (p - \alpha)\bigr) \vee \bigl(\forall x < y,\ x y \mid \alpha \Rightarrow n x \le \alpha y\bigr)\Bigr)$
Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000353.json: it records an attempt, not a proof (see Attempts below).

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/Witness.lean, sha256 d5cc8608e87c.
import Mathlib
import Nodes.«erdos-402--h3-v2--h1--h1--h1--h2».Context

open Filter

theorem witness : ∃ B : Finset ℕ, 0 ∉ B ∧ B.Nonempty ∧ B.gcd id = 1 ∧ ¬ B.card.Prime ∧
    (∀ q : ℕ, q.Prime → B.card ≠ q + 1) ∧
    (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) ∧
    (∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) := by
  have hc : ({1, 2, 3, 4, 5, 6, 7, 8, 9, 10} : Finset ℕ).card = 10 := by decide
  refine ⟨{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}, by decide, ⟨1, by decide⟩, by decide, ?_, ?_, ?_, ?_⟩
  · rw [hc]
    norm_num
  · intro q hq h
    rw [hc] at h
    have hq9 : q = 9 := by omega
    rw [hq9] at hq
    norm_num at hq
  · intro a ha b hb
    rw [hc]
    simp only [Finset.mem_insert, Finset.mem_singleton] at ha
    have ha10 : a ≤ 10 := by omega
    have hg : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (by omega)
    calc a ≤ 10 := ha10
      _ ≤ 10 * a.gcd b := Nat.le_mul_of_pos_right 10 hg
  · intro a ha p k hp hdvd
    rw [hc]
    simp only [Finset.mem_insert, Finset.mem_singleton] at ha
    have ha0 : 0 < a := by omega
    have hle : p ^ k ≤ a := Nat.le_of_dvd ha0 hdvd
    have hne : p ^ k ≠ 10 := by
      intro h10
      have hk : k ≠ 0 := by
        rintro rfl
        simp at h10
      have hp10 : p ∣ 10 := by
        rw [← h10]
        exact dvd_pow_self p hk
      have hp10' : p ≤ 10 := Nat.le_of_dvd (by norm_num) hp10
      have hk4 : k < 4 := by
        have h2 : 2 ^ k ≤ p ^ k := Nat.pow_le_pow_left hp.two_le k
        by_contra hk4
        push Not at hk4
        have h16 : 2 ^ 4 ≤ 2 ^ k := Nat.pow_le_pow_right (by norm_num) hk4
        omega
      have hp2 := hp.two_le
      interval_cases p <;> interval_cases k <;> simp_all (config := { decide := true })
    omega

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Attempts (1)

1 recorded. Routes refuted: none. Failure classes: none.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1001-402a; merged in fa5bb722c239 under attestations/000353.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20261001T170100Z-t1001-402a-partial.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. hall have (∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y) ∧ (∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y) ∧ ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y

    Leaves ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with hall : (∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y) ∧ (∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y) ∧ ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Uses library Finset Finset α is the type of finite sets of elements of α. , id The identity function. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

    Lean, lines 34–88
      have hall : (∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y)) := by
    refine ⟨?_, ?_, ?_⟩
    · have hs1 : ∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs1
    · have hs2 : ∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs2
    · have hlarge : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
        sorry
      exact hlarge

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 34–88 at 841d05f96fd2 ↗

    1. hall.s1 case

      Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.

      Lean, lines 59–65
          · have hs1 : ∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs1

      targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 59–65 at 841d05f96fd2 ↗

      1. hall.s1.hs1 hole ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y hole

        Leaves ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with hs1 : ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.

        Left open as a hole; its statement is erdos-402--h3-v2--h1--h1--h1--h2--h1 (proved).

        Lean, lines 59–64
            · have hs1 : ∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry

        targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 59–64 at 841d05f96fd2 ↗

    2. hall.s2 case

      Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.

      Lean, lines 66–72
          · have hs2 : ∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs2

      targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 66–72 at 841d05f96fd2 ↗

      1. hall.s2.hs2 hole ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y hole

        Leaves ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, with hs2 : ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y.

        Left open as a hole; its statement is erdos-402--h3-v2--h1--h1--h1--h2--h2 (proved).

        Lean, lines 66–71
            · have hs2 : ∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry

        targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 66–71 at 841d05f96fd2 ↗

    3. hall.s3 case

      Leaves ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

      Lean, lines 73–88
          · have hlarge : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
        sorry
      exact hlarge

      targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 73–88 at 841d05f96fd2 ↗

      1. hall.s3.hlarge hole ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y hole

        Leaves ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with hlarge : ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

        Uses library Finset Finset α is the type of finite sets of elements of α. , id The identity function. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. .

        Left open as a hole; its statement is erdos-402--h3-v2--h1--h1--h1--h2--h3 (open).

        Lean, lines 73–87
            · have hlarge : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
        sorry

        targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 73–87 at 841d05f96fd2 ↗

  2. s2 obtain (∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y) ∧ (∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y) ∧ ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y

    Leaves ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with hs1 : ∀ (n : ℕ), (10 : ℕ) ≤ n → n ≤ (228 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, hs2 : ∀ (n : ℕ), (229 : ℕ) ≤ n → n ≤ (200014 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p < (2 : ℕ) * n ∧ (2 : ℕ) * ((2 : ℕ) * n - p) ≤ n + (2 : ℕ) ∧ ∀ α < n, p < α + n → (∃ (q : ℕ), Nat.Prime q ∧ n ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → n * x ≤ α * y, hlarge : ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (200014 : ℕ) < B.card → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Lean, line 89
      obtain ⟨hs1, hs2, hlarge⟩ := hall

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 89 at 841d05f96fd2 ↗

  3. s3 case

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Lean, line 92
      · exact hlarge B h0 hne hg hnp hq hle hpk hbig

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 92 at 841d05f96fd2 ↗

  4. s4 case

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Uses library Or.inr Or.inr is "right injection" into an Or. .

    Lean, line 94
      · exact Or.inr (hs2 B.card c229 (by omega))

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 94 at 841d05f96fd2 ↗

  5. s5 case

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Uses library Or.inr Or.inr is "right injection" into an Or. .

    Lean, line 96
      · exact Or.inr (hs1 B.card c10 (by omega))

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 96 at 841d05f96fd2 ↗

  6. s6 case

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Uses library Or.inl Or.inl is "left injection" into an Or. , Exists.intro Existential introduction. .

    Lean, lines 98–101
      · obtain ⟨a, ha⟩ := hne
    refine Or.inl ⟨a, ha, a, ha, ?_⟩
    rw [h1]
    simp

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 98–101 at 841d05f96fd2 ↗

    1. s6.s1 obtain B.Nonempty

      Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with a : ℕ, ha : a ∈ B.

      Lean, line 98
        · obtain ⟨a, ha⟩ := hne

      targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 98 at 841d05f96fd2 ↗

  7. s7 case

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y.

    Uses library Or.inr Or.inr is "right injection" into an Or. , Exists.intro Existential introduction. .

    Lean, lines 103–104
      · refine Or.inr ⟨17, by norm_num, by omega, by omega, by omega, fun α h1 h2 => ?_⟩
    omega

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 103–104 at 841d05f96fd2 ↗

  8. hpos have (0 : ℕ) < B.card

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with hpos : (0 : ℕ) < B.card.

    Uses library Finset.card_pos.

    Lean, line 105
      have hpos : 0 < B.card := Finset.card_pos.mpr hne

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 105 at 841d05f96fd2 ↗

  9. x2 have B.card ≠ (2 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x2 : B.card ≠ (2 : ℕ).

    Lean, lines 106–109
      have x2 : B.card ≠ 2 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 106–109 at 841d05f96fd2 ↗

  10. x3 have B.card ≠ (3 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x3 : B.card ≠ (3 : ℕ).

    Lean, lines 110–113
      have x3 : B.card ≠ 3 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 110–113 at 841d05f96fd2 ↗

  11. x5 have B.card ≠ (5 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x5 : B.card ≠ (5 : ℕ).

    Lean, lines 114–117
      have x5 : B.card ≠ 5 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 114–117 at 841d05f96fd2 ↗

  12. x7 have B.card ≠ (7 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x7 : B.card ≠ (7 : ℕ).

    Lean, lines 118–121
      have x7 : B.card ≠ 7 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, lines 118–121 at 841d05f96fd2 ↗

  13. x4 have B.card ≠ (4 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x4 : B.card ≠ (4 : ℕ).

    Lean, line 122
      have x4 : B.card ≠ 4 := hq 3 (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 122 at 841d05f96fd2 ↗

  14. x6 have B.card ≠ (6 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x6 : B.card ≠ (6 : ℕ).

    Lean, line 123
      have x6 : B.card ≠ 6 := hq 5 (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 123 at 841d05f96fd2 ↗

  15. x8 have B.card ≠ (8 : ℕ)

    Leaves (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card < p ∧ p < (2 : ℕ) * B.card ∧ (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧ ∀ α < B.card, p < α + B.card → (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨ ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y, with x8 : B.card ≠ (8 : ℕ).

    Lean, line 124
      have x8 : B.card ≠ 8 := hq 7 (by norm_num)

    targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean, line 124 at 841d05f96fd2 ↗

import Mathlib
import Nodes.«erdos-402--h3-v2--h1--h1--h1--h2».Context

open Filter

/-! Hole `hgen` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_402__h3_v2__h1__h1__h1__h2 : ∀ (B : Finset ℕ),
  (0 : ℕ) ∉ B →
    B.Nonempty →
      B.gcd id = (1 : ℕ) →
        ¬Nat.Prime B.card →
          (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
            (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
              (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                  ∃ (p : ℕ),
                    Nat.Prime p ∧
                      B.card < p ∧
                        p < (2 : ℕ) * B.card ∧
                          (2 : ℕ) * ((2 : ℕ) * B.card - p) ≤ B.card + (2 : ℕ) ∧
                            ∀ α < B.card,
                              p < α + B.card →
                                (∃ (q : ℕ), Nat.Prime q ∧ B.card ≤ (3 : ℕ) * q ∧ q ∣ α * (p - α)) ∨
                                  ∀ (x y : ℕ), x < y → x * y ∣ α → B.card * x ≤ α * y := by
  -- Split of `hgen` by size n = |B| (agent 402-R6-a; statements prepared with agents 402-R5-b and 402-R6-b). Three holes,
  -- each in its own goal so none inherits another:
  -- `hs1` (10 ≤ n ≤ 228) and `hs2` (229 ≤ n ≤ 200014): a prime with the generalised window hypotheses exists. Finite
  -- certificates; both have complete Lean proofs ready.
  -- `hlarge` (n > 200014): the node's own conclusion for large sets. This is NOT a finite check and not a small lemma: it
  -- needs, for every large n, a prime within about √n below 2n, which no unconditional theorem gives; see the annex on it.
  -- The assembly proves the sizes below 10 and the case split.
  have hall : (∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y))
      ∧ (∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y)) := by
    refine ⟨?_, ?_, ?_⟩
    · have hs1 : ∀ n : ℕ, 10 ≤ n → n ≤ 228 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs1
    · have hs2 : ∀ n : ℕ, 229 ≤ n → n ≤ 200014 →
          ∃ p : ℕ, p.Prime ∧ n < p ∧ p < 2 * n ∧ 2 * (2 * n - p) ≤ n + 2 ∧
            ∀ α : ℕ, α < n → p < α + n →
              (∃ q : ℕ, q.Prime ∧ n ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
              (∀ x y : ℕ, x < y → x * y ∣ α → n * x ≤ α * y) := by
        sorry
      exact hs2
    · have hlarge : ∀ (B : Finset ℕ),
    (0 : ℕ) ∉ B →
      B.Nonempty →
        B.gcd id = (1 : ℕ) →
          ¬Nat.Prime B.card →
            (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
              (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
                (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
                  200014 < B.card →
                    (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨
                    ∃ p : ℕ, p.Prime ∧ B.card < p ∧ p < 2 * B.card ∧ 2 * (2 * B.card - p) ≤ B.card + 2 ∧
                      ∀ α : ℕ, α < B.card → p < α + B.card →
                        (∃ q : ℕ, q.Prime ∧ B.card ≤ 3 * q ∧ q ∣ α * (p - α)) ∨
                        (∀ x y : ℕ, x < y → x * y ∣ α → B.card * x ≤ α * y) := by
        sorry
      exact hlarge
  obtain ⟨hs1, hs2, hlarge⟩ := hall
  intro B h0 hne hg hnp hq hle hpk
  by_cases hbig : 200014 < B.card
  · exact hlarge B h0 hne hg hnp hq hle hpk hbig
  by_cases c229 : 229 ≤ B.card
  · exact Or.inr (hs2 B.card c229 (by omega))
  by_cases c10 : 10 ≤ B.card
  · exact Or.inr (hs1 B.card c10 (by omega))
  by_cases h1 : B.card = 1
  · obtain ⟨a, ha⟩ := hne
    refine Or.inl ⟨a, ha, a, ha, ?_⟩
    rw [h1]
    simp
  by_cases h9 : B.card = 9
  · refine Or.inr ⟨17, by norm_num, by omega, by omega, by omega, fun α h1 h2 => ?_⟩
    omega
  have hpos : 0 < B.card := Finset.card_pos.mpr hne
  have x2 : B.card ≠ 2 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x3 : B.card ≠ 3 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x5 : B.card ≠ 5 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x7 : B.card ≠ 7 := by
    intro h
    rw [h] at hnp
    exact hnp (by norm_num)
  have x4 : B.card ≠ 4 := hq 3 (by norm_num)
  have x6 : B.card ≠ 6 := hq 5 (by norm_num)
  have x8 : B.card ≠ 8 := hq 7 (by norm_num)
  omega
How to read this page

No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).

How to read a statement’s page →