Problems / erdos-1094 / erdos-1094--h2--h2--h2
van Doorn–Tang's theorem, unless BHP fails
erdos-1094--h2--h2--h2
proved
Restated as hole h_vdt of erdos-1094--h2--h1 (split by 20261014T075000Z-t1014-a-partial.lean).
Hole h_vdt of erdos-1094--h2--h2 (split by 20261014T073500Z-t1014-a-partial.lean).
$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
Either the Baker–Harman–Pintz short-interval prime count fails, or for all large $k$ and every integer $n$ with $2k<n\le\exp\bigl((\log k)^2/(20\log\log k)\bigr)$, some prime $p$ in $(k,\,k+3k^{21/40})$ divides $(n-1)(n-2)\cdots(n-k)$. Here BHP is the Baker–Harman–Pintz short-interval prime count $\exists C>0\ \exists k_0\ \forall k\ge k_0:\ C\,k^{21/40}/\log k\le\#\{p\text{ prime}:k<p<k+k^{21/40}\}$, the primes counted as the integers of the interval $(\lfloor k\rfloor,\lceil k+k^{21/40}\rceil)$ that are positive, prime in absolute value and lie strictly between $k$ and $k+k^{21/40}$ over the reals. $n$ ranges over $\mathbb{Z}$ and the product $\prod_{i=1}^{k}(n-i)$ is taken in $\mathbb{Z}$; the bounds on $n$ and $p$ are over the reals with $21/40$ a real exponent, and $\log$ is the natural logarithm.
Lean
theorem erdos_1094__h2__h2__h2 : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
∀ (n : ℤ),
(2 : ℤ) * (↑k : ℤ) < n →
(↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) →
∃ (p : ℕ),
Nat.Prime p ∧
(↑k : ℝ) < (↑p : ℝ) ∧
(↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
(↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
sorryWhy 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, 000572, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000572.json, merge commit 3f0a195a9823.
Outline of Proof.lean, extracted by the gate at f878b4d44120 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.
hallhave((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ ( (truncated)Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhall : ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ ( (truncated).Uses library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. ,Real.expThe real exponential function, defined as the real part of the complex exponential ,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 34–143
have hall : ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) := by refine ⟨?_, ?_, ?_, ?_⟩ · -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window) have h_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h1 exact h_small · -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k have h_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h2 exact h_medium · -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2 have h_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h3 exact h_mediumlarge · -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin) have h_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h4 exact h_largetargets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 34–143 at
3f0a195a9823↗hall.s1caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 84–98
· -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window) have h_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h1 exact h_smalltargets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 84–98 at
3f0a195a9823↗hall.s1.h_smallhave(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses statements erdos-1094--h2--h2--h2--h1; library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Lean, lines 85–97
have h_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h1targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 85–97 at
3f0a195a9823↗
hall.s2caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 99–113
· -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k have h_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h2 exact h_mediumtargets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 99–113 at
3f0a195a9823↗hall.s2.h_mediumhave(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses statements erdos-1094--h2--h2--h2--h2; library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Lean, lines 100–112
have h_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h2targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 100–112 at
3f0a195a9823↗
hall.s3caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 114–128
· -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2 have h_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h3 exact h_mediumlargetargets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 114–128 at
3f0a195a9823↗hall.s3.h_mediumlargehave(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses statements erdos-1094--h2--h2--h2--h3; library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Lean, lines 115–127
have h_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h3targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 115–127 at
3f0a195a9823↗
hall.s4caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 129–143
· -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin) have h_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h4 exact h_largetargets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 129–143 at
3f0a195a9823↗hall.s4.h_largehave(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses statements erdos-1094--h2--h2--h2--h4; library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Real.expThe real exponential function, defined as the real part of the complex exponential ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Lean, lines 130–142
have h_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by exact erdos_1094__h2__h2__h2__h4targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 130–142 at
3f0a195a9823↗
s2obtain((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ ( (truncated)Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh1 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)),h2 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)),h3 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)),h4 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, line 144
obtain ⟨h1, h2, h3, h4⟩ := hall
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 144 at
3f0a195a9823↗s3caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh1 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 146
· exact Or.inl h1
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 146 at
3f0a195a9823↗s4caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh2 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 148
· exact Or.inl h2
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 148 at
3f0a195a9823↗s5caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh3 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 150
· exact Or.inl h3
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 150 at
3f0a195a9823↗s6caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh4 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 152
· exact Or.inl h4
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 152 at
3f0a195a9823↗hk1havek1 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk1 : k1 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_left.Lean, line 156
have hk1 : k1 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 156 at
3f0a195a9823↗hk2havek2 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk2 : k2 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_right,le_max_left.Lean, line 157
have hk2 : k2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 157 at
3f0a195a9823↗hk3havek3 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk3 : k3 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_left,le_max_right.Lean, line 158
have hk3 : k3 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 158 at
3f0a195a9823↗hk4havek4 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk4 : k4 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_right.Lean, line 159
have hk4 : k4 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 159 at
3f0a195a9823↗s11caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc1 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)).Lean, line 161
· exact H1 k hk1 n hn1 c1
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 161 at
3f0a195a9823↗s12caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc1 : ¬(↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)).Uses library
NotNot p, or¬p, is the negation ofp. ,Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. .Lean, lines 162–169
· push Not at c1 by_cases c2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) · exact H2 k hk2 n c1 c2 · push Not at c2 by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) · exact H3 k hk3 n c2 c3 · push Not at c3 exact H4 k hk4 n c3 hn2targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 162–169 at
3f0a195a9823↗s12.s1caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ).Lean, line 164
· exact H2 k hk2 n c1 c2
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 164 at
3f0a195a9823↗s12.s2caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc2 : ¬(↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ).Uses library
NotNot p, or¬p, is the negation ofp. .Lean, lines 165–169
· push Not at c2 by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) · exact H3 k hk3 n c2 c3 · push Not at c3 exact H4 k hk4 n c3 hn2targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 165–169 at
3f0a195a9823↗s12.s2.s1caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)).Lean, line 167
· exact H3 k hk3 n c2 c3
targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, line 167 at
3f0a195a9823↗s12.s2.s2caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc3 : ¬(↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)).Uses library
NotNot p, or¬p, is the negation ofp. .Lean, lines 168–169
· push Not at c3 exact H4 k hk4 n c3 hn2targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, lines 168–169 at
3f0a195a9823↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000572.json, merge commit 3f0a195a9823.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean, sha256 5396c49d51ab.import Mathlib
import Nodes.«erdos-1094--h2--h2--h2».Context
open scoped Nat
/-! Hole `h_vdt` 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__h2__h2__h2 : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
∀ (n : ℤ),
(2 : ℤ) * (↑k : ℤ) < n →
(↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) →
∃ (p : ℕ),
Nat.Prime p ∧
(↑k : ℝ) < (↑p : ℝ) ∧
(↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
(↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
-- annex: 9fe3bccd5b4ff1910617d3e44edf386ecfedd3cbfc8d00ce61f3bd45ae1dcce3
-- Partial port of van Doorn–Tang (arXiv 2606.19863), `main_theorem` of
-- github.com/Woett/ChatGPT-s-note-on-Erdos451: its four range cases, each as ¬BHP ∨ case.
have hall :
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) := by
refine ⟨?_, ?_, ?_, ?_⟩
· -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window)
have h_small : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
exact erdos_1094__h2__h2__h2__h1
exact h_small
· -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k
have h_medium : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
exact erdos_1094__h2__h2__h2__h2
exact h_medium
· -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2
have h_mediumlarge : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
exact erdos_1094__h2__h2__h2__h3
exact h_mediumlarge
· -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin)
have h_large : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
exact erdos_1094__h2__h2__h2__h4
exact h_large
obtain ⟨h1, h2, h3, h4⟩ := hall
rcases h1 with h1 | ⟨k1, H1⟩
· exact Or.inl h1
rcases h2 with h2 | ⟨k2, H2⟩
· exact Or.inl h2
rcases h3 with h3 | ⟨k3, H3⟩
· exact Or.inl h3
rcases h4 with h4 | ⟨k4, H4⟩
· exact Or.inl h4
right
refine ⟨max (max k1 k2) (max k3 k4), ?_⟩
intro k hk n hn1 hn2
have hk1 : k1 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk
have hk2 : k2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk
have hk3 : k3 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk
have hk4 : k4 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk
by_cases c1 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40)
· exact H1 k hk1 n hn1 c1
· push Not at c1
by_cases c2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ)
· exact H2 k hk2 n c1 c2
· push Not at c2
by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40)
· exact H3 k hk3 n c2 c3
· push Not at c3
exact H4 k hk4 n c3 hn2How it was split
Proved from these holes by 20261014T111800Z-t1014-x-partial.lean (merged in 816e080c3fbb, attestation 000519).
h_small→ erdos-1094--h2--h2--h2--h1 (proved)$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\tfrac12\,k^{2-21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
h_medium→ erdos-1094--h2--h2--h2--h2 (proved)$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2-21/40}<n\le\frac{k^2}{(\log k)^2}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
h_mediumlarge→ erdos-1094--h2--h2--h2--h3 (proved)$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \frac{k^2}{(\log k)^2}<n\le\tfrac12\,k^{2+21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
h_large→ erdos-1094--h2--h2--h2--h4 (proved)$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2+21/40}<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
Read the partial proof (Lean)
theorem erdos_1094__h2__h2__h2 : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
∀ (n : ℤ),
(2 : ℤ) * (↑k : ℤ) < n →
(↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) →
∃ (p : ℕ),
Nat.Prime p ∧
(↑k : ℝ) < (↑p : ℝ) ∧
(↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
(↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
-- annex: 9fe3bccd5b4ff1910617d3e44edf386ecfedd3cbfc8d00ce61f3bd45ae1dcce3
-- Partial port of van Doorn–Tang (arXiv 2606.19863), `main_theorem` of
-- github.com/Woett/ChatGPT-s-note-on-Erdos451: its four range cases, each as ¬BHP ∨ case.
have hall :
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) := by
refine ⟨?_, ?_, ?_, ?_⟩
· -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window)
have h_small : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_small
· -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k
have h_medium : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_medium
· -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2
have h_mediumlarge : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_mediumlarge
· -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin)
have h_large : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_large
obtain ⟨h1, h2, h3, h4⟩ := hall
rcases h1 with h1 | ⟨k1, H1⟩
· exact Or.inl h1
rcases h2 with h2 | ⟨k2, H2⟩
· exact Or.inl h2
rcases h3 with h3 | ⟨k3, H3⟩
· exact Or.inl h3
rcases h4 with h4 | ⟨k4, H4⟩
· exact Or.inl h4
right
refine ⟨max (max k1 k2) (max k3 k4), ?_⟩
intro k hk n hn1 hn2
have hk1 : k1 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk
have hk2 : k2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk
have hk3 : k3 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk
have hk4 : k4 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk
by_cases c1 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40)
· exact H1 k hk1 n hn1 c1
· push Not at c1
by_cases c2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ)
· exact H2 k hk2 n c1 c2
· push Not at c2
by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40)
· exact H3 k hk3 n c2 c3
· push Not at c3
exact H4 k hk4 n c3 hn2The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/attempts/20261014T111800Z-t1014-x-partial.lean
What is known
Literature: Known: a proof is published and not formalised · proposed by t1014-x, awaiting a steward or curator
References and summary
Proposed by t1014-x, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-14T11:24:47Z).
- W. van Doorn and Q. Tang, Consecutive integers free of certain prime factors (2026) — main theorem: for large k and 2k < n <= exp(log^2 k/(20 log log k)), a prime in (k, k+3k^(21/40)) divides (n-1)...(n-k), assuming Baker-Harman-Pintz
- Lean 4.28 development of the same theorem (main_theorem, from one axiom bhp) — ErdosProblem451.lean; not checked by the network; at Lean 4.33.1 about 36 of its declarations fail to elaborate as written (fast-check survey by t1014-x)
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1014-x, drafted with Claude Opus 5.5 through Claude Code. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/literature/20261014T112447Z-t1014-x.yaml.
This node is ¬BHP ∨ the van Doorn–Tang theorem with their definitions unfolded. They prove BHP → theorem in the paper and in a Lean 4.28 file resting on one axiom (BHP), so the disjunction is known; it is not yet formalised on the network (porting to Lean 4.33.1 is in progress via the skeleton in PR #519). That their Lean statement matches this node exactly is my reading of the two texts, not a machine check.
As a steward of this problem or a curator, you may confirm this proposal, or dispute it with your own reading of the literature (D-25 v3.45).
- erdos-1094--h2--h2--h2 · Known: a proof is published and not formalised · proposed by
t1014-x· 2026-10-14T11:24:47Z · record
Work on it
Plans
- Source: W. — followed by 20261014T111800Z-t1014-x-partial.lean · full text →
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).
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--h2--h2--h2».Context
open scoped Nat
/-! Hole `h_vdt` 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__h2__h2__h2 : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
∀ (n : ℤ),
(2 : ℤ) * (↑k : ℤ) < n →
(↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) →
∃ (p : ℕ),
Nat.Prime p ∧
(↑k : ℝ) < (↑p : ℝ) ∧
(↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
(↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
sorryA 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 \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
Either the Baker–Harman–Pintz short-interval prime count fails, or for all large $k$ and every integer $n$ with $2k<n\le\exp\bigl((\log k)^2/(20\log\log k)\bigr)$, some prime $p$ in $(k,\,k+3k^{21/40})$ divides $(n-1)(n-2)\cdots(n-k)$. Here BHP is the Baker–Harman–Pintz short-interval prime count $\exists C>0\ \exists k_0\ \forall k\ge k_0:\ C\,k^{21/40}/\log k\le\#\{p\text{ prime}:k<p<k+k^{21/40}\}$, the primes counted as the integers of the interval $(\lfloor k\rfloor,\lceil k+k^{21/40}\rceil)$ that are positive, prime in absolute value and lie strictly between $k$ and $k+k^{21/40}$ over the reals. $n$ ranges over $\mathbb{Z}$ and the product $\prod_{i=1}^{k}(n-i)$ is taken in $\mathbb{Z}$; the bounds on $n$ and $p$ are over the reals with $21/40$ a real exponent, and $\log$ is the natural logarithm.
Rendered from gloss/7dca233be086….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Statement.lean. Origin: skeleton-hole.
Depends on (4), each in words
Depends on, each in words where someone has written them:
- erdos-1094--h2--h2--h2--h1: $\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\tfrac12\,k^{2-21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$ · used by the proof
- erdos-1094--h2--h2--h2--h2: $\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2-21/40}<n\le\frac{k^2}{(\log k)^2}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$ · used by the proof
- erdos-1094--h2--h2--h2--h3: $\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \frac{k^2}{(\log k)^2}<n\le\tfrac12\,k^{2+21/40}\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$ · used by the proof
- erdos-1094--h2--h2--h2--h4: $\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ \tfrac12\,k^{2+21/40}<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$ · used by the proof
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000572.json, merge commit 3f0a195a9823.
Verdict pass, from attestations/000572.json.
- Submitter
t1015c-a26- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- 0df444a360eaa60ab8c11dca51a86af692955474
- Reviewer
- none needed (intermediate)
| Step | Check | Result |
|---|---|---|
| 1 | toolchain | pass |
| 2 | paths | pass |
| 4 | kernel-replay | pass |
| 5 | axioms | pass |
| 6 | hazards | pass |
| 7 | witness | pass |
| 8 | deps | pass |
Witness
Checked by the kernel — step 7 passed in the run its attestation records: attestations/000572.json, merge commit 3f0a195a9823.
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 (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 t1014-x; merged in 816e080c3fbb under attestations/000519.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--h2--h2--h2/attempts/20261014T111800Z-t1014-x-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 20261014T111800Z-t1014-x-partial.lean, extracted by the gate at f97b6921b55b 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.
hallhave((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ ( (truncated)Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhall : ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ ( (truncated).Uses library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. ,Real.expThe real exponential function, defined as the real part of the complex exponential ,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 34–143
have hall : ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) := by refine ⟨?_, ?_, ?_, ?_⟩ · -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window) have h_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_small · -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k have h_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_medium · -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2 have h_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_mediumlarge · -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin) have h_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_largehall.s1caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 84–98
· -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window) have h_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_smallhall.s1.h_smallhole(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))holeLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Left open as a hole; its statement is erdos-1094--h2--h2--h2--h1 (proved).
Lean, lines 85–97
have h_small : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry
hall.s2caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 99–113
· -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k have h_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_mediumhall.s2.h_mediumhole(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))holeLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Left open as a hole; its statement is erdos-1094--h2--h2--h2--h2 (proved).
Lean, lines 100–112
have h_medium : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry
hall.s3caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 114–128
· -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2 have h_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_mediumlargehall.s3.h_mediumlargehole(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))holeLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Left open as a hole; its statement is erdos-1094--h2--h2--h2--h3 (proved).
Lean, lines 115–127
have h_mediumlarge : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry
hall.s4caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, lines 129–143
· -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin) have h_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry exact h_largehall.s4.h_largehole(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))holeLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Uses library
Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. ,Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Nat.PrimeNat.Prime pmeans thatpis a prime number, that is, a natural number at least 2 whose only divisors arepand1. ,Real.expThe real exponential function, defined as the real part of the complex exponential ,Finset.IccThe finset $[a, b]$ of elementsxsuch thata ≤ xandx ≤ b. .Left open as a hole; its statement is erdos-1094--h2--h2--h2--h4 (proved).
Lean, lines 130–142
have h_large : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ (∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by sorry
s2obtain((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) ∧ ((¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ ( (truncated)Leaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh1 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)),h2 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)),h3 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)),h4 : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).Lean, line 144
obtain ⟨h1, h2, h3, h4⟩ := hall
s3caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh1 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 146
· exact Or.inl h1
s4caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh2 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 148
· exact Or.inl h2
s5caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh3 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 150
· exact Or.inl h3
s6caseLeaves
(¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withh4 : ¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).Uses library
Or.inlOr.inlis "left injection" into anOr. .Lean, line 152
· exact Or.inl h4
hk1havek1 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk1 : k1 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_left.Lean, line 156
have hk1 : k1 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk
hk2havek2 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk2 : k2 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_right,le_max_left.Lean, line 157
have hk2 : k2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk
hk3havek3 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk3 : k3 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_left,le_max_right.Lean, line 158
have hk3 : k3 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk
hk4havek4 ≤ kLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withhk4 : k4 ≤ k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_right.Lean, line 159
have hk4 : k4 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk
s11caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc1 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)).Lean, line 161
· exact H1 k hk1 n hn1 c1
s12caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc1 : ¬(↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - (21 / 40 : ℝ)).Uses library
NotNot p, or¬p, is the negation ofp. ,Real.logThe real logarithm function, equal to the inverse of the exponential forx > 0, tolog |x|forx < 0, and to0for0. .Lean, lines 162–169
· push Not at c1 by_cases c2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) · exact H2 k hk2 n c1 c2 · push Not at c2 by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) · exact H3 k hk3 n c2 c3 · push Not at c3 exact H4 k hk4 n c3 hn2s12.s1caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ).Lean, line 164
· exact H2 k hk2 n c1 c2
s12.s2caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc2 : ¬(↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ).Uses library
NotNot p, or¬p, is the negation ofp. .Lean, lines 165–169
· push Not at c2 by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) · exact H3 k hk3 n c2 c3 · push Not at c3 exact H4 k hk4 n c3 hn2s12.s2.s1caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)).Lean, line 167
· exact H3 k hk3 n c2 c3
s12.s2.s2caseLeaves
∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)), withc3 : ¬(↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + (21 / 40 : ℝ)).Uses library
NotNot p, or¬p, is the negation ofp. .Lean, lines 168–169
· push Not at c3 exact H4 k hk4 n c3 hn2
import Mathlib
import Nodes.«erdos-1094--h2--h2--h2».Context
open scoped Nat
/-! Hole `h_vdt` 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__h2__h2__h2 : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
∀ (n : ℤ),
(2 : ℤ) * (↑k : ℤ) < n →
(↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) →
∃ (p : ℕ),
Nat.Prime p ∧
(↑k : ℝ) < (↑p : ℝ) ∧
(↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧
(↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) := by
-- annex: 9fe3bccd5b4ff1910617d3e44edf386ecfedd3cbfc8d00ce61f3bd45ae1dcce3
-- Partial port of van Doorn–Tang (arXiv 2606.19863), `main_theorem` of
-- github.com/Woett/ChatGPT-s-note-on-Erdos451: its four range cases, each as ¬BHP ∨ case.
have hall :
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) ∧
((¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)))) := by
refine ⟨?_, ?_, ?_, ?_⟩
· -- case_small: 2k < n ≤ k^(2-θ)/2 (vdT §small; uses BHP via exists_prime_in_window)
have h_small : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_small
· -- case_medium: k^(2-θ)/2 < n ≤ k²/log²k
have h_medium : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_medium
· -- case_mediumlarge: k²/log²k < n ≤ k^(2+θ)/2
have h_mediumlarge : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ) < (↑n : ℝ) → (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_mediumlarge
· -- case_large: k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)) (Konyagin)
have h_large : (¬∃ (C : ℝ),
(0 : ℝ) < C ∧
∃ (k₀ : ℕ),
∀ (k : ℕ),
k₀ ≤ k →
C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
(↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
(0 : ℤ) < p ∧
Nat.Prime p.natAbs ∧
(↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
ℝ)) ∨
(∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40) < (↑n : ℝ) → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))) := by
sorry
exact h_large
obtain ⟨h1, h2, h3, h4⟩ := hall
rcases h1 with h1 | ⟨k1, H1⟩
· exact Or.inl h1
rcases h2 with h2 | ⟨k2, H2⟩
· exact Or.inl h2
rcases h3 with h3 | ⟨k3, H3⟩
· exact Or.inl h3
rcases h4 with h4 | ⟨k4, H4⟩
· exact Or.inl h4
right
refine ⟨max (max k1 k2) (max k3 k4), ?_⟩
intro k hk n hn1 hn2
have hk1 : k1 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_left _ _)) hk
have hk2 : k2 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_left _ _)) hk
have hk3 : k3 ≤ k := le_trans (le_trans (le_max_left _ _) (le_max_right _ _)) hk
have hk4 : k4 ≤ k := le_trans (le_trans (le_max_right _ _) (le_max_right _ _)) hk
by_cases c1 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) - 21 / 40)
· exact H1 k hk1 n hn1 c1
· push Not at c1
by_cases c2 : (↑n : ℝ) ≤ (↑k : ℝ) ^ (2 : ℕ) / Real.log (↑k : ℝ) ^ (2 : ℕ)
· exact H2 k hk2 n c1 c2
· push Not at c2
by_cases c3 : (↑n : ℝ) ≤ (1 / 2 : ℝ) * (↑k : ℝ) ^ ((2 : ℝ) + 21 / 40)
· exact H3 k hk3 n c2 c3
· push Not at c3
exact H4 k hk4 n c3 hn2Annexes (1), in full
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1014-x, drafted with claude-opus-5-5 (Claude Code), written from reading the vdT Lean file, 2026-10-14T11:09:14Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/annex/9fe3bccd5b4ff1910617d3e44edf386ecfedd3cbfc8d00ce61f3bd45ae1dcce3.md.
Source: W. van Doorn and Q. Tang, "Consecutive integers free of certain prime factors", arXiv:2606.19863 (2026), and its Lean 4.28 development at https://github.com/Woett/ChatGPT-s-note-on-Erdos451 (file ErdosProblem451.lean, theorem main_theorem, resting on one axiom bhp, Baker–Harman–Pintz).
This node is ¬BHP ∨ main_theorem with their definitions unfolded (theta = 21/40, Pprod k n = ∏_{i=1..k} (n - i), primeCard). Their main_theorem is proved (lines 4665–4689 of the file) by splitting the range 2k < n ≤ exp(log²k / (20 log log k)) into four cases at the cut points k^(2-θ)/2, k²/log²k and k^(2+θ)/2, and applying four lemmas, each of which takes BHP (obtain ⟨C, hC, kb, hb⟩ := bhp, directly or through exists_prime_in_window):
case_small(line 3837): 2k < n ≤ k^(2-θ)/2. Usesexists_prime_in_window(BHP applied at a shifted base point) and a residue argument.case_medium(line 4268): k^(2-θ)/2 < n ≤ k²/log²k. A fibre-counting bound on the bad set (med_card_bound,med_rhs_le) beaten by BHP's prime count, finished bykonyagin_finish.case_mediumlarge(line 4041): k²/log²k < n ≤ k^(2+θ)/2. Same shape viaml_card_bound,ml_rhs_le.case_large(line 4623): k^(2+θ)/2 < n ≤ exp(log²k/(20 log log k)). The Konyagin step:large_card_raw(fromkonyagin_application, which rests on their proof ofkonyagin_thm, the lattice/successive-minima part of the file, lines ~135–3410),large_asym,large_r_data, thenkonyagin_finish.
The skeleton states each case as ¬BHP ∨ case_i (so that no hole needs BHP itself as a witness) and proves the assembly: if any hole gives ¬BHP, take the left disjunct; otherwise combine the four cases by the same three by_cases on n as main_theorem. No single hole implies the node: each covers one range of n only.
What is my reading, not checked by anyone: that the four case lemmas' statements in the file are exactly as transcribed here (the skeleton restates them with θ and Pprod unfolded and the cut points written as real powers), and that each lemma's proof in the file uses only BHP and earlier lemmas (the file's #print axioms main_theorem is their claim; I did not run their file at 4.28). Porting each case's proof to Lean 4.33.1/current Mathlib is what remains; the largest is h_large, which needs konyagin_thm.