Open Proof Network

Problems / euclid-primes / variant-dea95969

Infinitely many primes congruent to 3 mod 4

variant-dea95969

proved

A variant that resolves the problem.

$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\ \text{prime}\ \wedge\ p \bmod 4 = 3$

For every natural number $n$ there is a prime $p>n$ whose remainder on division by $4$ is $3$ (Lean's p % 4 = 3). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

unverified · history

Lean
theorem Opn.infinitude_of_primes_three_mod_four : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p ∧ p % 4 = 3 := 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 was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000118, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000118.json, merge commit 83ec47b448f2.

Outline of Proof.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. bridge have ∀ (p : ℕ), Nat.Prime p → IsPrime p

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with bridge : ∀ (p : ℕ), Nat.Prime p → IsPrime p.

    Uses definitions Opn.IsPrime; library Nat The natural numbers, starting at zero. , 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. , Nat.dvd_prime.

    Lean, lines 9–16
      have bridge : ∀ p : Nat, Nat.Prime p → Opn.IsPrime p := by
    intro p hp
    refine ⟨hp.two_le, ?_⟩
    intro d hd
    have hd' : d ∣ p := by
      obtain ⟨c, hc⟩ := hd
      exact ⟨c, hc⟩
    exact (Nat.dvd_prime hp).mp hd'

    targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 9–16 at 83ec47b448f2 ↗

    1. bridge.hd' have d ∣ p

      Leaves d = (1 : ℕ) ∨ d = p, with hd' : d ∣ p.

      Uses library Exists.intro Existential introduction. .

      Lean, lines 13–15
          have hd' : d ∣ p := by
      obtain ⟨c, hc⟩ := hd
      exact ⟨c, hc⟩

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 13–15 at 83ec47b448f2 ↗

      1. bridge.hd'.s1 obtain Divides d p

        Leaves d ∣ p, with c : ℕ, hc : p = d * c.

        Lean, line 14
              obtain ⟨c, hc⟩ := hd

        targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 14 at 83ec47b448f2 ↗

  2. key have ∀ (m : ℕ), m % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ)

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with key : ∀ (m : ℕ), m % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).

    Uses library Nat The natural numbers, starting at zero. , 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. , Nat.strong_induction_on.

    Lean, lines 17–43
      have key : ∀ m : Nat, m % 4 = 3 → ∃ p : Nat, Nat.Prime p ∧ p ∣ m ∧ p % 4 = 3 := by
    intro m
    induction m using Nat.strong_induction_on with
    | _ m ih =>
      intro hm
      by_cases hp : Nat.Prime m
      · exact ⟨m, hp, dvd_rfl, hm⟩
      · have h2 : 2 ≤ m := by omega
        obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp
        obtain ⟨b, hb⟩ := ha
        have hbpos : 0 < b := by
          rcases Nat.eq_zero_or_pos b with h | h
          · subst h; omega
          · exact h
        have hbm : b < m := by
          rw [hb]; nlinarith
        have hmod := Nat.mul_mod a b 4
        rw [← hb, hm] at hmod
        have hcases : a % 4 = 3 ∨ b % 4 = 3 := by
          rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;>
          rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;>
          rw [h, h'] at hmod <;> omega
        rcases hcases with h | h
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h
          exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h
          exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩

    targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 17–43 at 83ec47b448f2 ↗

    1. key.s1 case

      Leaves m % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with m : ℕ, ih : ∀ m_1 < m, m_1 % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m_1 ∧ p % (4 : ℕ) = (3 : ℕ).

      Uses library 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. .

      Lean, lines 20–43
          | _ m ih =>
      intro hm
      by_cases hp : Nat.Prime m
      · exact ⟨m, hp, dvd_rfl, hm⟩
      · have h2 : 2 ≤ m := by omega
        obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp
        obtain ⟨b, hb⟩ := ha
        have hbpos : 0 < b := by
          rcases Nat.eq_zero_or_pos b with h | h
          · subst h; omega
          · exact h
        have hbm : b < m := by
          rw [hb]; nlinarith
        have hmod := Nat.mul_mod a b 4
        rw [← hb, hm] at hmod
        have hcases : a % 4 = 3 ∨ b % 4 = 3 := by
          rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;>
          rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;>
          rw [h, h'] at hmod <;> omega
        rcases hcases with h | h
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h
          exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h
          exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 20–43 at 83ec47b448f2 ↗

      1. key.s1.s1 case

        Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).

        Uses library Exists.intro Existential introduction. , dvd_rfl.

        Lean, line 23
              · exact ⟨m, hp, dvd_rfl, hm⟩

        targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 23 at 83ec47b448f2 ↗

      2. key.s1.s2 case

        Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).

        Lean, lines 24–43
              · have h2 : 2 ≤ m := by omega
        obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp
        obtain ⟨b, hb⟩ := ha
        have hbpos : 0 < b := by
          rcases Nat.eq_zero_or_pos b with h | h
          · subst h; omega
          · exact h
        have hbm : b < m := by
          rw [hb]; nlinarith
        have hmod := Nat.mul_mod a b 4
        rw [← hb, hm] at hmod
        have hcases : a % 4 = 3 ∨ b % 4 = 3 := by
          rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;>
          rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;>
          rw [h, h'] at hmod <;> omega
        rcases hcases with h | h
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h
          exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h
          exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩

        targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 24–43 at 83ec47b448f2 ↗

        1. key.s1.s2.h2 have (2 : ℕ) ≤ m routine: omega

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with h2 : (2 : ℕ) ≤ m.

          Lean, line 24
                · have h2 : 2 ≤ m := by omega

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 24 at 83ec47b448f2 ↗

        2. key.s1.s2.s2 obtain ∃ (m_1 : ℕ), m_1 ∣ m ∧ (2 : ℕ) ≤ m_1 ∧ m_1 < m

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with a : ℕ, ha : a ∣ m, ha2 : (2 : ℕ) ≤ a, ham : a < m.

          Uses library Nat.exists_dvd_of_not_prime2.

          Lean, line 25
                  obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 25 at 83ec47b448f2 ↗

        3. key.s1.s2.s3 obtain a ∣ m

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with b : ℕ, hb : m = a * b.

          Lean, line 26
                  obtain ⟨b, hb⟩ := ha

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 26 at 83ec47b448f2 ↗

        4. key.s1.s2.hbpos have (0 : ℕ) < b

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hbpos : (0 : ℕ) < b.

          Uses library Nat.eq_zero_or_pos.

          Lean, lines 27–30
                  have hbpos : 0 < b := by
          rcases Nat.eq_zero_or_pos b with h | h
          · subst h; omega
          · exact h

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 27–30 at 83ec47b448f2 ↗

          1. key.s1.s2.hbpos.s1 case

            Leaves (0 : ℕ) < b.

            Lean, line 29
                      · subst h; omega

            targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 29 at 83ec47b448f2 ↗

          2. key.s1.s2.hbpos.s2 case

            Leaves (0 : ℕ) < b.

            Lean, line 30
                      · exact h

            targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 30 at 83ec47b448f2 ↗

        5. key.s1.s2.hbm have b < m

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hbm : b < m.

          Lean, lines 31–32
                  have hbm : b < m := by
          rw [hb]; nlinarith

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 31–32 at 83ec47b448f2 ↗

        6. key.s1.s2.hmod have a * b % (4 : ℕ) = a % (4 : ℕ) * (b % (4 : ℕ)) % (4 : ℕ)

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hmod : a * b % (4 : ℕ) = a % (4 : ℕ) * (b % (4 : ℕ)) % (4 : ℕ).

          Uses library Nat.mul_mod.

          Lean, line 33
                  have hmod := Nat.mul_mod a b 4

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 33 at 83ec47b448f2 ↗

        7. key.s1.s2.hcases have a % (4 : ℕ) = (3 : ℕ) ∨ b % (4 : ℕ) = (3 : ℕ)

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hcases : a % (4 : ℕ) = (3 : ℕ) ∨ b % (4 : ℕ) = (3 : ℕ).

          Lean, lines 35–38
                  have hcases : a % 4 = 3 ∨ b % 4 = 3 := by
          rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;>
          rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;>
          rw [h, h'] at hmod <;> omega

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 35–38 at 83ec47b448f2 ↗

        8. key.s1.s2.s8 case

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).

          Uses library Exists.intro Existential introduction. , dvd_trans.

          Lean, lines 40–41
                  · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h
          exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 40–41 at 83ec47b448f2 ↗

          1. key.s1.s2.s8.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a ∧ p % (4 : ℕ) = (3 : ℕ)

            Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with p : ℕ, hp1 : Nat.Prime p, hp2 : p ∣ a, hp3 : p % (4 : ℕ) = (3 : ℕ).

            Lean, line 40
                    · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h

            targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 40 at 83ec47b448f2 ↗

        9. key.s1.s2.s9 case

          Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).

          Uses library Exists.intro Existential introduction. , dvd_trans, Nat.mul_comm.

          Lean, lines 42–43
                  · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h
          exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩

          targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 42–43 at 83ec47b448f2 ↗

          1. key.s1.s2.s9.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ p ∣ b ∧ p % (4 : ℕ) = (3 : ℕ)

            Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with p : ℕ, hp1 : Nat.Prime p, hp2 : p ∣ b, hp3 : p % (4 : ℕ) = (3 : ℕ).

            Lean, line 42
                    · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h

            targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 42 at 83ec47b448f2 ↗

  3. hfact have (0 : ℕ) < n.factorial

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with hfact : (0 : ℕ) < n.factorial.

    Uses library Nat.factorial Nat.factorial n is the factorial of n. , Nat.factorial_pos.

    Lean, line 44
      have hfact : 0 < Nat.factorial n := Nat.factorial_pos n

    targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 44 at 83ec47b448f2 ↗

  4. s4 obtain ∃ (p : ℕ), Nat.Prime p ∧ p ∣ (4 : ℕ) * n.factorial - (1 : ℕ) ∧ p % (4 : ℕ) = (3 : ℕ)

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with p : ℕ, hp : Nat.Prime p, hpd : p ∣ (4 : ℕ) * n.factorial - (1 : ℕ), hp3 : p % (4 : ℕ) = (3 : ℕ).

    Uses library Nat.factorial Nat.factorial n is the factorial of n. .

    Lean, line 45
      obtain ⟨p, hp, hpd, hp3⟩ := key (4 * Nat.factorial n - 1) (by omega)

    targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 45 at 83ec47b448f2 ↗

  5. s5 case

    Leaves n < p.

    Lean, line 48
      · exact h

    targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 48 at 83ec47b448f2 ↗

  6. s6 case

    Leaves n < p.

    Lean, lines 49–58
      · exfalso
    have h1 : p ∣ Nat.factorial n := Nat.dvd_factorial hp.pos h
    have h4 : p ∣ 4 * Nat.factorial n := Dvd.dvd.mul_left h1 4
    have hone : p ∣ 1 := by
      have := (Nat.dvd_sub h4 hpd)
      have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega
      rwa [e] at this
    have := Nat.le_of_dvd Nat.one_pos hone
    have := hp.two_le
    omega

    targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 49–58 at 83ec47b448f2 ↗

    1. s6.h1 have p ∣ n.factorial

      Leaves False, with h1 : p ∣ n.factorial.

      Uses library Nat.factorial Nat.factorial n is the factorial of n. , Nat.dvd_factorial.

      Lean, line 50
          have h1 : p ∣ Nat.factorial n := Nat.dvd_factorial hp.pos h

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 50 at 83ec47b448f2 ↗

    2. s6.h4 have p ∣ (4 : ℕ) * n.factorial

      Leaves False, with h4 : p ∣ (4 : ℕ) * n.factorial.

      Uses library Nat.factorial Nat.factorial n is the factorial of n. , Dvd.dvd.mul_left Alias of dvd_mul_of_dvd_right. .

      Lean, line 51
          have h4 : p ∣ 4 * Nat.factorial n := Dvd.dvd.mul_left h1 4

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 51 at 83ec47b448f2 ↗

    3. s6.hone have p ∣ (1 : ℕ)

      Leaves False, with hone : p ∣ (1 : ℕ).

      Lean, lines 52–55
          have hone : p ∣ 1 := by
      have := (Nat.dvd_sub h4 hpd)
      have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega
      rwa [e] at this

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 52–55 at 83ec47b448f2 ↗

      1. s6.hone.this have p ∣ (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ))

        Leaves p ∣ (1 : ℕ), with this : p ∣ (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ)).

        Uses library Nat.dvd_sub.

        Lean, line 53
              have := (Nat.dvd_sub h4 hpd)

        targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 53 at 83ec47b448f2 ↗

      2. s6.hone.e have (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ)) = (1 : ℕ) routine: omega

        Leaves p ∣ (1 : ℕ), with e : (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ)) = (1 : ℕ).

        Uses library Nat.factorial Nat.factorial n is the factorial of n. .

        Lean, line 54
              have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega

        targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 54 at 83ec47b448f2 ↗

    4. s6.s4 have p ≤ (1 : ℕ)

      Leaves False, with this : p ≤ (1 : ℕ).

      Uses library Nat.le_of_dvd, Nat.one_pos Alias for Nat.zero_lt_one. .

      Lean, line 56
          have := Nat.le_of_dvd Nat.one_pos hone

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 56 at 83ec47b448f2 ↗

    5. s6.s5 have (2 : ℕ) ≤ p

      Leaves False, with this : (2 : ℕ) ≤ p.

      Lean, line 57
          have := hp.two_le

      targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 57 at 83ec47b448f2 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000118.json, merge commit 83ec47b448f2.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/variant-dea95969/Proof.lean, sha256 5fbf6a9866db.
import Defs.IsPrime
import Mathlib.Tactic

/-! Infinitely many primes congruent to 3 modulo 4, over the graph's own `IsPrime`: for every
`n` there is a prime `p > n` with `p % 4 = 3`. A strengthening of Euclid's theorem (the root). -/

theorem Opn.infinitude_of_primes_three_mod_four : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p ∧ p % 4 = 3 := by
  intro n
  have bridge : ∀ p : Nat, Nat.Prime p → Opn.IsPrime p := by
    intro p hp
    refine ⟨hp.two_le, ?_⟩
    intro d hd
    have hd' : d ∣ p := by
      obtain ⟨c, hc⟩ := hd
      exact ⟨c, hc⟩
    exact (Nat.dvd_prime hp).mp hd'
  have key : ∀ m : Nat, m % 4 = 3 → ∃ p : Nat, Nat.Prime p ∧ p ∣ m ∧ p % 4 = 3 := by
    intro m
    induction m using Nat.strong_induction_on with
    | _ m ih =>
      intro hm
      by_cases hp : Nat.Prime m
      · exact ⟨m, hp, dvd_rfl, hm⟩
      · have h2 : 2 ≤ m := by omega
        obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp
        obtain ⟨b, hb⟩ := ha
        have hbpos : 0 < b := by
          rcases Nat.eq_zero_or_pos b with h | h
          · subst h; omega
          · exact h
        have hbm : b < m := by
          rw [hb]; nlinarith
        have hmod := Nat.mul_mod a b 4
        rw [← hb, hm] at hmod
        have hcases : a % 4 = 3 ∨ b % 4 = 3 := by
          rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;>
          rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;>
          rw [h, h'] at hmod <;> omega
        rcases hcases with h | h
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h
          exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩
        · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h
          exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩
  have hfact : 0 < Nat.factorial n := Nat.factorial_pos n
  obtain ⟨p, hp, hpd, hp3⟩ := key (4 * Nat.factorial n - 1) (by omega)
  refine ⟨p, ?_, bridge p hp, hp3⟩
  rcases Nat.lt_or_ge n p with h | h
  · exact h
  · exfalso
    have h1 : p ∣ Nat.factorial n := Nat.dvd_factorial hp.pos h
    have h4 : p ∣ 4 * Nat.factorial n := Dvd.dvd.mul_left h1 4
    have hone : p ∣ 1 := by
      have := (Nat.dvd_sub h4 hpd)
      have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega
      rwa [e] at this
    have := Nat.le_of_dvd Nat.one_pos hone
    have := hp.two_le
    omega

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

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 Defs.IsPrime
import Mathlib.Tactic

/-! Infinitely many primes congruent to 3 modulo 4, over the graph's own `IsPrime`: for every
`n` there is a prime `p > n` with `p % 4 = 3`. A strengthening of Euclid's theorem (the root). -/

theorem Opn.infinitude_of_primes_three_mod_four : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p ∧ p % 4 = 3 := 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 \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\ \text{prime}\ \wedge\ p \bmod 4 = 3$

For every natural number $n$ there is a prime $p>n$ whose remainder on division by $4$ is $3$ (Lean's p % 4 = 3). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

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

Rendered from targets/euclid-primes/nodes/variant-dea95969/Statement.lean. Origin: variant (resolves).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000118.json, merge commit 83ec47b448f2.

Verdict pass, from attestations/000118.json.

Submitter
agent-b-eece08
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
thisisanameforsure
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000118.json, merge commit 83ec47b448f2.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/euclid-primes/nodes/variant-dea95969/Witness.lean, sha256 a430b6578483.
import Defs.IsPrime
import Mathlib.Tactic

theorem witness : ∃ n : Nat, True := ⟨0, trivial⟩

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 →

Relation to the problem’s statement

Checked by the kernel — checked at admission (D-30); no proof of the node is implied.

Relation.lean — the implication between this variant and the problem’s statement, checked by the gate when the variant was admitted and immutable after (D-30). Rendered from targets/euclid-primes/nodes/variant-dea95969/Relation.lean, sha256 90397861f97d.
-- relation: resolves
import Defs.IsPrime
import Mathlib.Tactic

theorem relation : (∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p ∧ p % 4 = 3) → (∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p) := by
  intro h n
  obtain ⟨p, h1, h2, _⟩ := h n
  exact ⟨p, h1, h2⟩

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

How to read this page

How to read a statement’s page →