FormalConjectures.ErdosProblems.«394»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 394

References:

erdosproblems.com/394

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

[ErHa78] Erdős, P. and Hall, R. R., On some unconventional problems on the divisors of integers. J. Austral. Math. Soc. Ser. A (1978), 479--485.

open Nat Filter Finsetopen scoped Asymptotics Topology Natnamespace Erdos394

Let $t_k(n)$ denote the least $m$ such that $n\mid m(m+1)(m+2)\cdots (m+k-1).$

noncomputable def t (k n : ℕ) : ℕ :=
  sInf { m : ℕ | 0 < m ∧ n ∣ ∏ i ∈ range k, (m + i) }

t k n = v when v works and nothing positive below it does.

@[category API, AMS 11]
theorem t_eq_of {n k v : ℕ} (hv : 0 < v)
    (hdvd : n ∣ ∏ i ∈ range k, (v + i))
    (hlt : ∀ m ∈ range v, 0 < m → ¬ (n ∣ ∏ i ∈ range k, (m + i))) :
    t k n = v := byn:ℕk:ℕv:ℕhv:0 < vhdvd:n ∣ ∏ i ∈ range k, (v + i)hlt:∀ m ∈ range v, 0 < m → ¬n ∣ ∏ i ∈ range k, (m + i)⊢ t k n = v
  refine le_antisymm (Nat.sInf_le ⟨hv, hdvd⟩) ?_n:ℕk:ℕv:ℕhv:0 < vhdvd:n ∣ ∏ i ∈ range k, (v + i)hlt:∀ m ∈ range v, 0 < m → ¬n ∣ ∏ i ∈ range k, (m + i)⊢ v ≤ t k n
  by_contra! hcn:ℕk:ℕv:ℕhv:0 < vhdvd:n ∣ ∏ i ∈ range k, (v + i)hlt:∀ m ∈ range v, 0 < m → ¬n ∣ ∏ i ∈ range k, (m + i)hc:t k n < v⊢ False
  have hne : { m : ℕ | 0 < m ∧ n ∣ ∏ i ∈ range k, (m + i) }.Nonempty := ⟨v, hv, hdvd⟩n:ℕk:ℕv:ℕhv:0 < vhdvd:n ∣ ∏ i ∈ range k, (v + i)hlt:∀ m ∈ range v, 0 < m → ¬n ∣ ∏ i ∈ range k, (m + i)hc:t k n < vhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range k, (m + i)}.Nonempty⊢ False
  obtain ⟨hpos, hd⟩ := Nat.sInf_mem hnen:ℕk:ℕv:ℕhv:0 < vhdvd:n ∣ ∏ i ∈ range k, (v + i)hlt:∀ m ∈ range v, 0 < m → ¬n ∣ ∏ i ∈ range k, (m + i)hc:t k n < vhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range k, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range k, (m + i)}hd:n ∣ ∏ i ∈ range k, (sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range k, (m + i)} + i)⊢ False
  exact hlt _ (mem_range.mpr hc) hpos hdAll goals completed! 🐙

The least positive multiple of n is n, so t 1 n = n.


@[category API, AMS 11]
theorem t_one {n : ℕ} (hn : 0 < n) : t 1 n = n := byn:ℕhn:0 < n⊢ t 1 n = n
  refine le_antisymm (Nat.sInf_le ⟨hn, byn:ℕhn:0 < n⊢ n ∣ ∏ i ∈ range 1, (n + i) simpAll goals completed! 🐙⟩) ?_
  have hne : { m : ℕ | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i) }.Nonempty := ⟨n, hn, byn:ℕhn:0 < n⊢ n ∣ ∏ i ∈ range 1, (n + i)n:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonempty⊢ n ≤ t 1 n simpAll goals completed! 🐙n:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonempty⊢ n ≤ t 1 n⟩n:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonempty⊢ n ≤ t 1 n
  obtain ⟨hpos, hd⟩ := Nat.sInf_mem hnen:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}hd:n ∣ ∏ i ∈ range 1, (sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)} + i)⊢ n ≤ t 1 n
  rw [prod_range_one,n:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}hd:n ∣ sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)} + 0⊢ n ≤ t 1 nn:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}hd:n ∣ sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}⊢ n ≤ t 1 n add_zeron:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}hd:n ∣ sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}⊢ n ≤ t 1 nn:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}hd:n ∣ sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}⊢ n ≤ t 1 n] at hdn:ℕhn:0 < nhne:{m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}.Nonemptyhpos:0 < sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}hd:n ∣ sInf {m | 0 < m ∧ n ∣ ∏ i ∈ range 1, (m + i)}⊢ n ≤ t 1 n
  exact Nat.le_of_dvd hpos hdAll goals completed! 🐙

Is it true that $\sum_{n\leq x}t_2(n)\ll \frac{x^2}{(\log x)^c}$ for some $c>0$?

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-394/Research/FirstQuestion.lean"]
theorem erdos_394.parts.i :
    answer(True) ↔
      ∃ c > 0, (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
      (t 2 n : ℝ)) ≪ (fun x ↦ x ^ 2 / (Real.log x) ^ c) := by⊢ True ↔ ∃ c > 0, (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, ↑(t 2 n)) =O[atTop] fun x ↦ ↑x ^ 2 / Real.log ↑x ^ c
  sorryAll goals completed! 🐙

Is it true that, for $k\geq 2$, $\sum_{n\leq x}t_{k+1}(n) =o\left(\sum_{n\leq x}t_k(n)\right)?$

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-394/Research/DenseHierarchyLittleO.lean"]
theorem erdos_394.parts.ii :
    answer(True) ↔
      ∀ k ≥ 2, (fun (x : ℝ) ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
      (t (k + 1) n : ℝ)) =o[atTop]
      (fun (x : ℝ) ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
      (t k n : ℝ)) := by⊢ True ↔ ∀ k ≥ 2, (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, ↑(t (k + 1) n)) =o[atTop] fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, ↑(t k n)
  sorryAll goals completed! 🐙

In [ErGr80] they mention a conjecture of Erdős that the sum is $o(x^2)$. This was proved by Erdős and Hall [ErHa78], who proved that in fact $\sum_{n\leq x}t_2(n)\ll \frac{\log\log\log x}{\log\log x}x^2.$

@[category research solved, AMS 11]
theorem erdos_394.variants.hall_bound :
    (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, (t 2 n : ℝ)) ≪
    (fun x ↦ x ^ 2 * (Real.log (Real.log (Real.log x)) / Real.log (Real.log x))) := by⊢ (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, ↑(t 2 n)) =O[atTop] fun x ↦
  ↑x ^ 2 * (Real.log (Real.log (Real.log ↑x)) / Real.log (Real.log ↑x))
  sorryAll goals completed! 🐙

Erdős and Hall conjecture that the sum is $o(x^2/(\log x)^c)$ for any $c<\log 2$.

@[category research open, AMS 11]
theorem erdos_394.variants.hall_conjecture :
    ∀ c < Real.log 2, (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊,
    (t 2 n : ℝ)) =o[atTop]
    (fun x ↦ x ^ 2 / (Real.log x) ^ c) := by⊢ ∀ c < Real.log 2, (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, ↑(t 2 n)) =o[atTop] fun x ↦ x ^ 2 / Real.log x ^ c
  sorryAll goals completed! 🐙

Since $t_2(p)=p-1$ for prime $p$ it is trivial that $\sum_{n\leq x}t_2(n)\gg \frac{x^2}{\log x}$.

@[category research solved, AMS 11]
theorem erdos_394.variants.lower_bound :
    (fun x ↦ x ^ 2 / Real.log x) ≪
    (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, (t 2 n : ℝ)) := by⊢ (fun x ↦ ↑x ^ 2 / Real.log ↑x) =O[atTop] fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, ↑(t 2 n)
  sorryAll goals completed! 🐙

They ask about the behaviour of $t_{n-3}(n!)$ and also ask whether, for infinitely many $n$, $t_k(n!)< t_{k-1}(n!)-1$ for all $1\leq k < n$.

@[category research open, AMS 11]
theorem erdos_394.variants.factorial_gap_conjecture :
    answer(sorry) ↔
      Set.Infinite { n : ℕ | ∀ k, 2 ≤ k → k < n →
      t k (n !) < t (k - 1) (n !) - 1 } := by⊢ True ↔ {n | ∀ (k : ℕ), 2 ≤ k → k < n → t k n ! < t (k - 1) n ! - 1}.Infinite
  sorryAll goals completed! 🐙

set_option maxRecDepth 20000 in

They proved (with Selfridge) that this holds for $n=10$.


@[category research solved, AMS 11]
theorem erdos_394.variants.factorial_gap_10 :
    ∀ (k : ℕ), 2 ≤ k → k < 10 →
    t k (10 !) <
    t (k - 1) (10 !) - 1 := by⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h1 : t 1 (10 !) = 3628800 := by rw [t_one⊢ 10! = 3628800⊢ 0 < 10!⊢ 10! = 3628800⊢ 0 < 10!h1:t 1 10! = 3628800⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1]⊢ 10! = 3628800⊢ 0 < 10!h1:t 1 10! = 3628800⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 <;>⊢ 10! = 3628800⊢ 0 < 10!h1:t 1 10! = 3628800⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_num [Nat.factorial]h1:t 1 10! = 3628800⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1h1:t 1 10! = 3628800⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h2 : t 2 (10 !) = 512000 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800⊢ t 2 3628800 = 512000h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800⊢ 0 < 512000h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800⊢ 3628800 ∣ ∏ i ∈ range 2, (512000 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 native_decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800⊢ ∀ m ∈ range 512000, 0 < m → ¬3628800 ∣ ∏ i ∈ range 2, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 native_decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h3 : t 3 (10 !) = 6398 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ t 3 3628800 = 6398h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ 0 < 6398h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ 3628800 ∣ ∏ i ∈ range 3, (6398 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 native_decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000⊢ ∀ m ∈ range 6398, 0 < m → ¬3628800 ∣ ∏ i ∈ range 3, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 native_decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h4 : t 4 (10 !) = 5373 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ t 4 3628800 = 5373h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ 0 < 5373h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ 3628800 ∣ ∏ i ∈ range 4, (5373 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 native_decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398⊢ ∀ m ∈ range 5373, 0 < m → ¬3628800 ∣ ∏ i ∈ range 4, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 native_decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h5 : t 5 (10 !) = 348 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ t 5 3628800 = 348h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ 0 < 348h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ 3628800 ∣ ∏ i ∈ range 5, (348 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373⊢ ∀ m ∈ range 348, 0 < m → ¬3628800 ∣ ∏ i ∈ range 5, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h6 : t 6 (10 !) = 160 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ t 6 3628800 = 160h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ 0 < 160h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ 3628800 ∣ ∏ i ∈ range 6, (160 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348⊢ ∀ m ∈ range 160, 0 < m → ¬3628800 ∣ ∏ i ∈ range 6, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h7 : t 7 (10 !) = 30 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ t 7 3628800 = 30h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ 0 < 30h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ 3628800 ∣ ∏ i ∈ range 7, (30 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160⊢ ∀ m ∈ range 30, 0 < m → ¬3628800 ∣ ∏ i ∈ range 7, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h8 : t 8 (10 !) = 9 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ t 8 3628800 = 9h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ 0 < 9h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ 3628800 ∣ ∏ i ∈ range 8, (9 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30⊢ ∀ m ∈ range 9, 0 < m → ¬3628800 ∣ ∏ i ∈ range 8, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  have h9 : t 9 (10 !) = 2 := by
    norm_num [Nat.factorial]h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ t 9 3628800 = 2h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1; exact t_eq_of (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ 0 < 2h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 norm_numAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ 3628800 ∣ ∏ i ∈ range 9, (2 + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1) (byh1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9⊢ ∀ m ∈ range 2, 0 < m → ¬3628800 ∣ ∏ i ∈ range 9, (m + i)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1 decideAll goals completed! 🐙h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1)h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2⊢ ∀ (k : ℕ), 2 ≤ k → k < 10 → t k 10! < t (k - 1) 10! - 1
  intro k hk2 hk10h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ khk10:k < 10⊢ t k 10! < t (k - 1) 10! - 1
  interval_cases k«2»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 2hk10:2 < 10⊢ t 2 10! < t (2 - 1) 10! - 1«3»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 3hk10:3 < 10⊢ t 3 10! < t (3 - 1) 10! - 1«4»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 4hk10:4 < 10⊢ t 4 10! < t (4 - 1) 10! - 1«5»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 5hk10:5 < 10⊢ t 5 10! < t (5 - 1) 10! - 1«6»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 6hk10:6 < 10⊢ t 6 10! < t (6 - 1) 10! - 1«7»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 7hk10:7 < 10⊢ t 7 10! < t (7 - 1) 10! - 1«8»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 8hk10:8 < 10⊢ t 8 10! < t (8 - 1) 10! - 1«9»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 9hk10:9 < 10⊢ t 9 10! < t (9 - 1) 10! - 1 <;>«2»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 2hk10:2 < 10⊢ t 2 10! < t (2 - 1) 10! - 1«3»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 3hk10:3 < 10⊢ t 3 10! < t (3 - 1) 10! - 1«4»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 4hk10:4 < 10⊢ t 4 10! < t (4 - 1) 10! - 1«5»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 5hk10:5 < 10⊢ t 5 10! < t (5 - 1) 10! - 1«6»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 6hk10:6 < 10⊢ t 6 10! < t (6 - 1) 10! - 1«7»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 7hk10:7 < 10⊢ t 7 10! < t (7 - 1) 10! - 1«8»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 8hk10:8 < 10⊢ t 8 10! < t (8 - 1) 10! - 1«9»h1:t 1 10! = 3628800h2:t 2 10! = 512000h3:t 3 10! = 6398h4:t 4 10! = 5373h5:t 5 10! = 348h6:t 6 10! = 160h7:t 7 10! = 30h8:t 8 10! = 9h9:t 9 10! = 2k:ℕhk2:2 ≤ 9hk10:9 < 10⊢ t 9 10! < t (9 - 1) 10! - 1 simp_allAll goals completed! 🐙

end Erdos394