Open Proof Network

Problems / erdos-1094 / erdos-1094--h3--h1--h1--h1

Residue form, k even, 3 | k

erdos-1094--h3--h1--h1--h1

open

Hole h_k6 of erdos-1094--h3--h1--h1 (split by 20261014T112100Z-t1014-z-partial.lean).

$\displaystyle \exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

For all large $k$ divisible by $2$ and by $3$, every $n$ with $2k\le n<k^2$ has a prime $p\le k$ whose residue of $n$ is smaller than its residue of $k$. Lean writes $k^2$ as k * k and the divisibilities as k % 2 = 0 and k % 3 = 0. n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$, a carry at the last base-$p$ digit when $k$ is subtracted from $n$ (hence $p \mid \binom{n}{k}$ by Kummer's theorem, though the statement names no binomial coefficient).

unverified · history

Lean
theorem erdos_1094__h3__h1__h1__h1 : ∃ (K₁ : ℕ),
  ∀ (n k : ℕ),
    K₁ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := 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 20261015T145000Z-t1015c-a12-partial.lean (merged in 5cc3798a54c1, attestation 000551).

  • h_k30 → erdos-1094--h3--h1--h1--h1--h1 (open)

    $\displaystyle \exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k,\ \ 5\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

  • h_k6rest → erdos-1094--h3--h1--h1--h1--h2 (open)

    $\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k,\ \ 5\nmid k,\ \ k \bmod 5 \le n \bmod 5 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

Read the partial proof (Lean)
theorem erdos_1094__h3__h1__h1__h1 : ∃ (K₁ : ℕ),
  ∀ (n k : ℕ),
    K₁ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have hall : (∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 → k % 3 = 0 →
        k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧
      (∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 → k % 3 = 0 →
        0 < k % 5 → k % 5 ≤ n % 5 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) := by
    refine ⟨?_, ?_⟩
    · have h_k30 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k30
    · have h_k6rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → 0 < k % 5 → k % 5 ≤ n % 5 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k6rest
  obtain ⟨K₁, h₁⟩ := hall.1
  obtain ⟨K₂, h₂⟩ := hall.2
  refine ⟨max K₁ (max K₂ 5), fun n k hk h2k hnk hk2 hk3 => ?_⟩
  have hK₁ : K₁ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hK₂ : K₂ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk5 : 5 ≤ k := le_of_lt (lt_of_le_of_lt (le_trans (le_max_right K₂ 5) (le_max_right _ _)) hk)
  by_cases h0 : k % 5 = 0
  · exact h₁ n k hK₁ h2k hnk hk2 hk3 h0
  · by_cases hlt : n % 5 < k % 5
    · exact ⟨5, Nat.prime_five, hk5, hlt⟩
    · exact h₂ n k hK₂ h2k hnk hk2 hk3 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-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-1094--h3--h1--h1--h1».Context

open scoped Nat

/-! Hole `h_k6` 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_1094__h3__h1__h1__h1 : ∃ (K₁ : ℕ),
  ∀ (n k : ℕ),
    K₁ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := 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 \exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

For all large $k$ divisible by $2$ and by $3$, every $n$ with $2k\le n<k^2$ has a prime $p\le k$ whose residue of $n$ is smaller than its residue of $k$. Lean writes $k^2$ as k * k and the divisibilities as k % 2 = 0 and k % 3 = 0. n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$, a carry at the last base-$p$ digit when $k$ is subtracted from $n$ (hence $p \mid \binom{n}{k}$ by Kummer's theorem, though the statement names no binomial coefficient).

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

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

Depends on (2), each in words

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

  • erdos-1094--h3--h1--h1--h1--h1: $\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k,\ \ 5\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
  • erdos-1094--h3--h1--h1--h1--h2: $\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\mid k,\ \ 5\nmid k,\ \ k \bmod 5 \le n \bmod 5 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000551.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-1094/nodes/erdos-1094--h3--h1--h1--h1/Witness.lean, sha256 1aa8a1c1b9f3.
import Mathlib

open scoped Nat

theorem witness : True := 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 →

Attempts (2)

2 recorded. Routes refuted: none. Failure classes: missing-library 1.

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 t1015c-a12; merged in 5cc3798a54c1 under attestations/000551.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-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-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 20261015T145000Z-t1015c-a12-partial.lean, extracted by the gate at 067497e74a8b 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 (∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p

    Leaves ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hall : (∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

    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. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

    Lean, lines 14–25
      have hall : (∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 → k % 3 = 0 →
        k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧
      (∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 → k % 3 = 0 →
        0 < k % 5 → k % 5 ≤ n % 5 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) := by
    refine ⟨?_, ?_⟩
    · have h_k30 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k30
    · have h_k6rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → 0 < k % 5 → k % 5 ≤ n % 5 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k6rest

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, lines 14–25 at f0dfc93f9827 ↗

    1. hall.s1 case

      Leaves ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

      Lean, lines 19–21
          · have h_k30 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k30

      targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, lines 19–21 at f0dfc93f9827 ↗

      1. hall.s1.h_k30 hole ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p hole

        Leaves ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_k30 : ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

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

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

        Lean, lines 19–20
            · have h_k30 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry

        targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, lines 19–20 at f0dfc93f9827 ↗

    2. hall.s2 case

      Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

      Lean, lines 22–25
          · have h_k6rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → 0 < k % 5 → k % 5 ≤ n % 5 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k6rest

      targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, lines 22–25 at f0dfc93f9827 ↗

      1. hall.s2.h_k6rest hole ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p hole

        Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_k6rest : ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

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

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

        Lean, lines 22–24
            · have h_k6rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → 0 < k % 5 → k % 5 ≤ n % 5 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry

        targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, lines 22–24 at f0dfc93f9827 ↗

  2. s2 obtain ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p

    Leaves ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with K₁ : ℕ, h₁ : ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → k % (5 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

    Lean, line 26
      obtain ⟨K₁, h₁⟩ := hall.1

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 26 at f0dfc93f9827 ↗

  3. s3 obtain ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p

    Leaves ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with K₂ : ℕ, h₂ : ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (5 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

    Lean, line 27
      obtain ⟨K₂, h₂⟩ := hall.2

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 27 at f0dfc93f9827 ↗

  4. hK1 have K₁ < k

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hK₁ : K₁ < k.

    Uses library lt_of_le_of_lt, le_max_left.

    Lean, line 29
      have hK₁ : K₁ < k := lt_of_le_of_lt (le_max_left _ _) hk

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 29 at f0dfc93f9827 ↗

  5. hK2 have K₂ < k

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hK₂ : K₂ < k.

    Uses library lt_of_le_of_lt, le_trans The relation ≤ on a preorder is transitive. , le_max_left, le_max_right.

    Lean, line 30
      have hK₂ : K₂ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 30 at f0dfc93f9827 ↗

  6. hk5 have (5 : ℕ) ≤ k

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hk5 : (5 : ℕ) ≤ k.

    Uses library le_of_lt, lt_of_le_of_lt, le_trans The relation ≤ on a preorder is transitive. , le_max_right.

    Lean, line 31
      have hk5 : 5 ≤ k := le_of_lt (lt_of_le_of_lt (le_trans (le_max_right K₂ 5) (le_max_right _ _)) hk)

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 31 at f0dfc93f9827 ↗

  7. s7 case

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h0 : k % (5 : ℕ) = (0 : ℕ).

    Lean, line 33
      · exact h₁ n k hK₁ h2k hnk hk2 hk3 h0

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 33 at f0dfc93f9827 ↗

  8. s8 case

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h0 : ¬k % (5 : ℕ) = (0 : ℕ).

    Lean, lines 34–36
      · by_cases hlt : n % 5 < k % 5
    · exact ⟨5, Nat.prime_five, hk5, hlt⟩
    · exact h₂ n k hK₂ h2k hnk hk2 hk3 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, lines 34–36 at f0dfc93f9827 ↗

    1. s8.s1 case

      Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hlt : n % (5 : ℕ) < k % (5 : ℕ).

      Uses library Exists.intro Existential introduction. , Nat.prime_five.

      Lean, line 35
          · exact ⟨5, Nat.prime_five, hk5, hlt⟩

      targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 35 at f0dfc93f9827 ↗

    2. s8.s2 case

      Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hlt : ¬n % (5 : ℕ) < k % (5 : ℕ).

      Uses library Nat.pos_of_ne_zero, Nat.le_of_not_lt.

      Lean, line 36
          · exact h₂ n k hK₂ h2k hnk hk2 hk3 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)

      targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean, line 36 at f0dfc93f9827 ↗

import Mathlib
import Nodes.«erdos-1094--h3--h1--h1--h1».Context

open scoped Nat

/-! Hole `h_k6` 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_1094__h3__h1__h1__h1 : ∃ (K₁ : ℕ),
  ∀ (n k : ℕ),
    K₁ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have hall : (∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 → k % 3 = 0 →
        k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧
      (∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 → k % 3 = 0 →
        0 < k % 5 → k % 5 ≤ n % 5 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) := by
    refine ⟨?_, ?_⟩
    · have h_k30 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → k % 5 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k30
    · have h_k6rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 0 →
          k % 3 = 0 → 0 < k % 5 → k % 5 ≤ n % 5 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_k6rest
  obtain ⟨K₁, h₁⟩ := hall.1
  obtain ⟨K₂, h₂⟩ := hall.2
  refine ⟨max K₁ (max K₂ 5), fun n k hk h2k hnk hk2 hk3 => ?_⟩
  have hK₁ : K₁ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hK₂ : K₂ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk5 : 5 ≤ k := le_of_lt (lt_of_le_of_lt (le_trans (le_max_right K₂ 5) (le_max_right _ _)) hk)
  by_cases h0 : k % 5 = 0
  · exact h₁ n k hK₁ h2k hnk hk2 hk3 h0
  · by_cases hlt : n % 5 < k % 5
    · exact ⟨5, Nat.prime_five, hk5, hlt⟩
    · exact h₂ n k hK₂ h2k hnk hk2 hk3 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)
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 →