Formalizing a proof of Erdos problem #379, arising from conversations between Stijn Cambie, Vjeko Kovac, and Terry Tao. See the discussion at https://www.erdosproblems.com/forum/thread/379

theorem binom_eq {n k : ℕ} (hk : 1 ≤ k) : n.choose k * k = (n - 1).choose (k - 1) * n

$$\binom{n}{k} \cdot k = \binom{n-1}{k-1} \cdot n$$.

theorem binom_eq_2 {n k : ℕ} (hk : 2 ≤ k) : n.choose k * k * (k - 1) = (n - 2).choose (k - 2) * (n - 1) * n

$$\binom{n}{k} \cdot k \cdot (k-1) = \binom{n-2}{k-2} \cdot (n-1) \cdot n$$.

theorem lemma_1 {n k p a b : ℕ} (hk : 1 ≤ k) (hp : Nat.Prime p) (h1 : p ^ (a + b + 1) ∣ n) : p ^ (a + 1) ∣ n.choose k ∨ p ^ (b + 1) ∣ k

If $$p^{a+b+1} \mid n$$, then $$p^{a+1} \mid \binom{n}{k}$$ or $$p^{b+1} \mid k$$.

theorem lemma_2 {n k p r : ℕ} (hk : 2 ≤ k) (hn : k ≤ n) (hp : Nat.Prime p) (h1 : p ^ r ∣ n - 1) (hr : 0 < r) (h2 : ¬p ∣ k) (h3 : ¬p ∣ n - k) : p ^ r ∣ n.choose k

If $$p^r \mid n-1$$ and $$k,n-k$$ are not divisible by $$p$$, then $$p^r \mid \binom{n}{k}$$.

theorem key_prop {k n p r R : ℕ} (hn : n = 2 ^ (p ^ R).totient) (hk : 1 ≤ k) (hkn : k < n) (hp : Nat.Prime p) (hpr : p > 2 ^ (r - 1)) (hr : 1 < r) (hr' : r ≤ (p ^ R).totient) : 2 ^ r ∣ n.choose k ∨ p ^ R ∣ n.choose k

If $$n=2^{\phi(p^R)}$$ and $$p>2^{r-1}$$, then $$2^r \mid \binom{n}{k}$$ or $$p^R \mid \binom{n}{k}$$.

@[reducible, inline]

noncomputable abbrev S (n : ℕ) : ℕ

Equations

• S n = sSup {r : ℕ | ∀ k ∈ Finset.Ico 1 n, ∃ (p : ℕ), Nat.Prime p ∧ p ^ r ∣ n.choose k}

theorem S_ge {n r : ℕ} (hn : 1 < n) (h : ∀ k ∈ Finset.Ico 1 n, ∃ (p : ℕ), Nat.Prime p ∧ p ^ r ∣ n.choose k) : r ≤ S n

The condition 1<n is necessary to avoid the range of k being vacuous.

theorem key_cor {p r : ℕ} (hp : Nat.Prime p) (hpr : p > 2 ^ (r - 1)) (hr : 1 < r) : r ≤ S (2 ^ (p ^ r).totient)

If $$p>2^{r-1}$$, then $$S(2^{\phi(p^R)}) \ge r$$.

theorem erdos_379 : Filter.limsup (fun (n : ℕ) => ↑(S n)) Filter.atTop = ⊤

A positive resolution to Erdos problem #379.