FormalConjectures.ErdosProblems.«686»

/-
Copyright 2025 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 686

References:

erdosproblems.com/686

[Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.


namespace Erdos686

Can every integer $N≥2$ be written as $$N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_686 :
    answer(sorry) ↔ ∀ N ≥ (2 : ℕ), ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
      (N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i)) := by⊢ True ↔ ∀ N ≥ 2, ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  sorryAll goals completed! 🐙

Can every square $N≥2$ be written as $$N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_686.variants.square :
    answer(sorry) ↔ ∀ N ≥ (2 : ℕ),  (IsSquare N) → ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
      (N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i)) := by⊢ True ↔
  ∀ N ≥ 2,
    IsSquare N → ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  sorryAll goals completed! 🐙

Can $4$ be written as $$4=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_686.variants.four :
    answer(sorry) ↔ ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
      (4 : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i)) := by⊢ True ↔ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 4 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  sorryAll goals completed! 🐙

The number $4$ cannot be written as $$4=\frac{\prod_{1\leq i\leq 2}(m+i)}{\prod_{1\leq i\leq 2}(n+i)}$$ for $m≥n+2$!

@[category research solved, AMS 11]
theorem erdos_686.variants.four_two :
    ¬ ∃ᵉ (n : ℕ) (m ≥ n + 2),
      (4 : ℚ) = (∏ i ∈ Finset.Icc 1 2, (m + i)) / (∏ i ∈ Finset.Icc 1 2, (n + i)) := by⊢ ¬∃ n, ∃ m ≥ n + 2, 4 = ↑(∏ i ∈ Finset.Icc 1 2, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 2, (n + i))
  simp only [Finset.prod_Icc_succ_top (by decide : 1 ≤ 2), Finset.Icc_self,
    Finset.prod_singleton]⊢ ¬∃ n, ∃ m ≥ n + 2, 4 = ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1)))
  push_neg⊢ ∀ (n m : ℕ), m ≥ n + 2 → 4 ≠ ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1)))
  intro n mn:ℕm:ℕ⊢ m ≥ n + 2 → 4 ≠ ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1))) hmn:ℕm:ℕhm:m ≥ n + 2⊢ 4 ≠ ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1)))
  rw [ne_eq, eq_div_iff (by positivity : (↑((n + 1) * (n + (1 + 1))) : ℚ) ≠ 0)]n:ℕm:ℕhm:m ≥ n + 2⊢ ¬4 * ↑((n + 1) * (n + (1 + 1))) = ↑((m + 1) * (m + (1 + 1)))
  push_castn:ℕm:ℕhm:m ≥ n + 2⊢ ¬4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)
  intro hn:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)⊢ False
  have h' : 4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2) := by⊢ ¬∃ n, ∃ m ≥ n + 2, 4 = ↑(∏ i ∈ Finset.Icc 1 2, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 2, (n + i)) exact_mod_cast hAll goals completed! 🐙
  by_cases hc : m < 2 * (n + 1)posn:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2) := 
  cast
    (Eq.trans
      (congr (congrArg (fun x => Eq (↑4 * ((↑n + x) * (↑n + ↑2)))) (Eq.symm Nat.cast_one))
        (congrArg (fun x => (↑m + x) * (↑m + ↑2)) (Eq.symm Nat.cast_one)))
      (Eq.trans
        (congr
          (congrArg Eq
            (Eq.trans
              (congrArg (HMul.hMul ↑4)
                (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 n 1)) (Nat.cast_add._simp_1 n 2))
                  (Nat.cast_mul._simp_1 (n + 1) (n + 2))))
              (Nat.cast_mul._simp_1 4 ((n + 1) * (n + 2)))))
          (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 m 1)) (Nat.cast_add._simp_1 m 2))
            (Nat.cast_mul._simp_1 (m + 1) (m + 2))))
        Nat.cast_inj._simp_1))
    hhc:m < 2 * (n + 1)⊢ Falsenegn:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2) := 
  cast
    (Eq.trans
      (congr (congrArg (fun x => Eq (↑4 * ((↑n + x) * (↑n + ↑2)))) (Eq.symm Nat.cast_one))
        (congrArg (fun x => (↑m + x) * (↑m + ↑2)) (Eq.symm Nat.cast_one)))
      (Eq.trans
        (congr
          (congrArg Eq
            (Eq.trans
              (congrArg (HMul.hMul ↑4)
                (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 n 1)) (Nat.cast_add._simp_1 n 2))
                  (Nat.cast_mul._simp_1 (n + 1) (n + 2))))
              (Nat.cast_mul._simp_1 4 ((n + 1) * (n + 2)))))
          (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 m 1)) (Nat.cast_add._simp_1 m 2))
            (Nat.cast_mul._simp_1 (m + 1) (m + 2))))
        Nat.cast_inj._simp_1))
    hhc:¬m < 2 * (n + 1)⊢ False <;>posn:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2) := 
  cast
    (Eq.trans
      (congr (congrArg (fun x => Eq (↑4 * ((↑n + x) * (↑n + ↑2)))) (Eq.symm Nat.cast_one))
        (congrArg (fun x => (↑m + x) * (↑m + ↑2)) (Eq.symm Nat.cast_one)))
      (Eq.trans
        (congr
          (congrArg Eq
            (Eq.trans
              (congrArg (HMul.hMul ↑4)
                (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 n 1)) (Nat.cast_add._simp_1 n 2))
                  (Nat.cast_mul._simp_1 (n + 1) (n + 2))))
              (Nat.cast_mul._simp_1 4 ((n + 1) * (n + 2)))))
          (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 m 1)) (Nat.cast_add._simp_1 m 2))
            (Nat.cast_mul._simp_1 (m + 1) (m + 2))))
        Nat.cast_inj._simp_1))
    hhc:m < 2 * (n + 1)⊢ Falsenegn:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2) := 
  cast
    (Eq.trans
      (congr (congrArg (fun x => Eq (↑4 * ((↑n + x) * (↑n + ↑2)))) (Eq.symm Nat.cast_one))
        (congrArg (fun x => (↑m + x) * (↑m + ↑2)) (Eq.symm Nat.cast_one)))
      (Eq.trans
        (congr
          (congrArg Eq
            (Eq.trans
              (congrArg (HMul.hMul ↑4)
                (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 n 1)) (Nat.cast_add._simp_1 n 2))
                  (Nat.cast_mul._simp_1 (n + 1) (n + 2))))
              (Nat.cast_mul._simp_1 4 ((n + 1) * (n + 2)))))
          (Eq.trans (congr (congrArg HMul.hMul (Nat.cast_add._simp_1 m 1)) (Nat.cast_add._simp_1 m 2))
            (Nat.cast_mul._simp_1 (m + 1) (m + 2))))
        Nat.cast_inj._simp_1))
    hhc:¬m < 2 * (n + 1)⊢ False nlinarithAll goals completed! 🐙

The number $4$ cannot be written as $$4=\frac{\prod_{1\leq i\leq 3}(m+i)}{\prod_{1\leq i\leq 3}(n+i)}$$ for $m≥n+3$!

See comment section on erdosproblems.com

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_686.variants.four_three :
    ¬ ∃ᵉ (n : ℕ) (m ≥ n + 3),
      (4 : ℚ) = (∏ i ∈ Finset.Icc 1 3, (m + i)) / (∏ i ∈ Finset.Icc 1 3, (n + i)) := by⊢ ¬∃ n, ∃ m ≥ n + 3, 4 = ↑(∏ i ∈ Finset.Icc 1 3, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 3, (n + i))
  sorryAll goals completed! 🐙

Can $9$ be written as $$9=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

@[category research solved, AMS 11]
theorem erdos_686.variants.nine :
    answer(True) ↔ ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
      (9 : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i)) := by⊢ True ↔ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 9 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  -- Witness: k = 3, n = 11, m = 25, since (26·27·28)/(12·13·14) = 19656/2184 = 9.
  simp only [true_iff]⊢ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 9 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  refine ⟨3, by⊢ 3 ≥ 2 norm_numAll goals completed! 🐙, 11, 25, by⊢ 25 ≥ 11 + 3 norm_numAll goals completed! 🐙, ?_⟩
  norm_num [Finset.prod_Icc_succ_top, Finset.Icc_self, Finset.prod_singleton]All goals completed! 🐙

Can $25$ be written as $$25=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_686.variants.twenty_five :
    answer(sorry) ↔ ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
      (25 : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i)) := by⊢ True ↔ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 25 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  sorryAll goals completed! 🐙

Can every non-square $N≥2$ be written as $$N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

@[category research solved, AMS 11]
theorem erdos_686.variants.non_square :
    answer(True) ↔ ∀ N ≥ (2 : ℕ), (¬ IsSquare N) → ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
      (N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i)) := by⊢ True ↔
  ∀ N ≥ 2,
    ¬IsSquare N → ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
  refine ⟨fun _ N hN_ge_2 hN_not_square => ?_, fun _ => trivial⟩x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare N⊢ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

  have hN_not_square' : ¬ ∃ s, s * s = N := fun ⟨s, hs⟩ => hN_not_square ⟨s, hs.symm⟩x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))⊢ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

  -- 1. Setup the existence for k = 2 and simplify the products
  exists 2, byx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))⊢ 2 ≥ 2 validAll goals completed! 🐙
  field_simpx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))⊢ ∃ n, ∃ m ≥ n + 2, ↑N = ↑(∏ i ∈ Finset.Icc 1 2, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 2, (n + i))
  simp [Finset.prod_Icc_succ_top, Finset.Icc_self, Finset.prod_singleton]x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))⊢ ∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))

  -- 2. Case split on the existence of solutions for small bounds
  by_cases h : {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyposx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ ∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))negx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ ∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))
  ·posx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ ∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2)) obtain rfl | hN_lt := hN_ge_2.eq_or_ltpos.inlx✝:TruehN_ge_2:2 ≥ 2hN_not_square:¬IsSquare 2hN_not_square':¬∃ s, s * s = 2h:{n | ∃ k, 2 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ ∃ n m, n + 2 ≤ m ∧ ↑2 = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))pos.inrx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < N⊢ ∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))
    ·pos.inlx✝:TruehN_ge_2:2 ≥ 2hN_not_square:¬IsSquare 2hN_not_square':¬∃ s, s * s = 2h:{n | ∃ k, 2 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ ∃ n m, n + 2 ≤ m ∧ ↑2 = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2)) exact mod_cast
        if a : ∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, _ then
          a.imp fun a s => s.2.imp fun and => And.right
        else
          byx✝:TruehN_ge_2:2 ≥ 2hN_not_square:¬IsSquare 2hN_not_square':¬∃ s, s * s = 2h:{n | ∃ k, 2 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptya:¬∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, a + 2 ≤ n ∧ 2 = ↑((n + 1) * (n + 2)) / ↑((a + 1) * (a + 2))⊢ ∃ n m, n + 2 ≤ m ∧ 2 = ↑((m + 1) * (m + 2)) / ↑((n + 1) * (n + 2)) exact (a (byx✝:TruehN_ge_2:2 ≥ 2hN_not_square:¬IsSquare 2hN_not_square':¬∃ s, s * s = 2h:{n | ∃ k, 2 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptya:¬∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, a + 2 ≤ n ∧ 2 = ↑((n + 1) * (n + 2)) / ↑((a + 1) * (a + 2))⊢ ∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, a + 2 ≤ n ∧ 2 = ↑((n + 1) * (n + 2)) / ↑((a + 1) * (a + 2)) native_decideAll goals completed! 🐙)).elim

    obtain rfl | hN_ne_3 := eq_or_ne N 3pos.inr.inlx✝:TruehN_ge_2:3 ≥ 2hN_not_square:¬IsSquare 3hN_not_square':¬∃ s, s * s = 3h:{n | ∃ k, 3 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < 3⊢ ∃ n m, n + 2 ≤ m ∧ ↑3 = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))pos.inr.inrx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < NhN_ne_3:N ≠ 3⊢ ∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))
    ·pos.inr.inlx✝:TruehN_ge_2:3 ≥ 2hN_not_square:¬IsSquare 3hN_not_square':¬∃ s, s * s = 3h:{n | ∃ k, 3 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < 3⊢ ∃ n m, n + 2 ≤ m ∧ ↑3 = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2)) exact mod_cast
        if a : ∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, _ then
          a.imp fun and μ => μ.2.imp fun and => And.right
        else
          byx✝:TruehN_ge_2:3 ≥ 2hN_not_square:¬IsSquare 3hN_not_square':¬∃ s, s * s = 3h:{n | ∃ k, 3 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < 3a:¬∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, a + 2 ≤ n ∧ 3 = ↑((n + 1) * (n + 2)) / ↑((a + 1) * (a + 2))⊢ ∃ n m, n + 2 ≤ m ∧ 3 = ↑((m + 1) * (m + 2)) / ↑((n + 1) * (n + 2)) exact (a (byx✝:TruehN_ge_2:3 ≥ 2hN_not_square:¬IsSquare 3hN_not_square':¬∃ s, s * s = 3h:{n | ∃ k, 3 * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < 3a:¬∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, a + 2 ≤ n ∧ 3 = ↑((n + 1) * (n + 2)) / ↑((a + 1) * (a + 2))⊢ ∃ a ∈ Finset.range 30, ∃ n ∈ Finset.range 30, a + 2 ≤ n ∧ 3 = ↑((n + 1) * (n + 2)) / ↑((a + 1) * (a + 2)) native_decideAll goals completed! 🐙)).elim

    exact h.mono fun and =>
      .imp fun a s =>
        mod_cast (byx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < NhN_ne_3:N ≠ 3and:ℕa:ℕs:N * ((and + 1) * (and + 2)) = (a + 1) * (a + 2)⊢ and + 2 ≤ a ∧ ↑N = ↑((a + 1) * (a + 2)) / ↑((and + 1) * (and + 2)) refine ⟨byx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < NhN_ne_3:N ≠ 3and:ℕa:ℕs:N * ((and + 1) * (and + 2)) = (a + 1) * (a + 2)⊢ and + 2 ≤ a
            nlinarith only [pow_three and, s, show N > 3 byx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < NhN_ne_3:N ≠ 3and:ℕa:ℕs:N * ((and + 1) * (and + 2)) = (a + 1) * (a + 2)⊢ and + 2 ≤ a validAll goals completed! 🐙], ?_⟩; push_cast [s.symm]x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.NonemptyhN_lt:2 < NhN_ne_3:N ≠ 3and:ℕa:ℕs:N * ((and + 1) * (and + 2)) = (a + 1) * (a + 2)⊢ ↑N = ↑N * ((↑and + 1) * (↑and + 2)) / ((↑and + 1) * (↑and + 2)); field_simpAll goals completed! 🐙)

  -- 3. Reduce the general case to Pell's Equation
  convert (Pell.exists_of_not_isSquare _)ax✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ (∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))) ↔
  ¬IsSquare ?neg.convert_1✝ → ∃ x y, x ^ 2 - ?neg.convert_1✝ * y ^ 2 = 1 ∧ y ≠ 0neg.convert_1x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ ℤneg.convert_2x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ 0 < ?neg.convert_1✝
  show @@_ ↔ ¬ IsSquare (N * 4 : ℤ) → _ax✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ (∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))) ↔
  ¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0neg.convert_2x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ 0 < ?neg.convert_1✝
  ·ax✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ (∃ n m, n + 2 ≤ m ∧ ↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))) ↔
  ¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0 use
      mod_cast h.elim ∘ .imp (fun n ⟨m, hle, heq⟩ => ⟨m, byx✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyn:ℕx✝:∃ m, n + 2 ≤ m ∧ ↑N = ↑((m + 1) * (m + 2)) / ↑((n + 1) * (n + 2))m:ℕhle:n + 2 ≤ mheq:↑N = ↑((m + 1) * (m + 2)) / ↑((n + 1) * (n + 2))⊢ N * ((n + 1) * (n + 2)) = (m + 1) * (m + 2)
        push_cast at heqx✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyn:ℕx✝:∃ m, n + 2 ≤ m ∧ ↑N = ↑((m + 1) * (m + 2)) / ↑((n + 1) * (n + 2))m:ℕhle:n + 2 ≤ mheq:↑N = (↑m + 1) * (↑m + 2) / ((↑n + 1) * (↑n + 2))⊢ N * ((n + 1) * (n + 2)) = (m + 1) * (m + 2); rw [eq_div_iff (by positivity : ((n : ℚ) + 1) * (↑n + 2) ≠ 0)] at heqx✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyn:ℕx✝:∃ m, n + 2 ≤ m ∧ ↑N = ↑((m + 1) * (m + 2)) / ↑((n + 1) * (n + 2))m:ℕhle:n + 2 ≤ mheq:↑N * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)⊢ N * ((n + 1) * (n + 2)) = (m + 1) * (m + 2)
        exact_mod_cast heqAll goals completed! 🐙⟩),
      (. (mod_cast hN_not_square' ∘ .rec (by⊢ True ↔
  ∀ N ≥ 2,
    ¬IsSquare N → ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
          use . / 2
          norm_num [←., true, Nat.div_mul_div_comm _, ((2).pow_dvd_pow_iff two_ne_zero).1, false, sq]))
        |>.elim ↑? _)

    use fun and ⟨A, B, _⟩ =>
      absurd
        (eq_add_of_sub_eq B)
        (A.natAbs_sq ▸ and.natAbs_sq ▸ mod_cast fun and => h ?_)mprx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty

    -- Parity analysis
    obtain ⟨l, hl⟩ | ⟨a, ha⟩ := ((byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2⊢ ℤ ·x✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2⊢ ℤ boundAll goals completed! 🐙 : ℤ)).natAbs.even_or_odd
    ·mpr.inlx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2l:ℕhl:and✝.natAbs = l + l⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty exact absurd
        (and.trans (byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2l:ℕhl:and✝.natAbs = l + l⊢ 1 + N * 4 * A.natAbs ^ 2 = ?m.563 rw [mul_right_comm]All goals completed! 🐙) |>.symm.trans (byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2l:ℕhl:and✝.natAbs = l + l⊢ and✝.natAbs ^ 2 = ?m.565 rw [(by valid :), sq, add_mul]All goals completed! 🐙))
        (byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2l:ℕhl:and✝.natAbs = l + l⊢ ¬1 + N * A.natAbs ^ 2 * 4 = l * (l + l) + l * (l + l) validAll goals completed! 🐙)

    match a with
    | 0 =>x✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2a:ℕha:and✝.natAbs = 2 * 0 + 1⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty simp_allAll goals completed! 🐙
    | S + 1 =>x✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2a:ℕS:ℕha:and✝.natAbs = 2 * (S + 1) + 1⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty
        use A.natAbs + S, N * A.natAbs + S, byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N := 
  fun x =>
    match x with
    | Exists.intro s hs => hN_not_square (Exists.intro s (Eq.symm hs))h:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonemptyx✝¹:¬IsSquare (↑N * 4) → ∃ x y, x ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0and✝:ℤx✝:∃ y, and✝ ^ 2 - ↑N * 4 * y ^ 2 = 1 ∧ y ≠ 0A:ℤB:and✝ ^ 2 - ↑N * 4 * A ^ 2 = 1right✝:A ≠ 0and:and✝.natAbs ^ 2 = 1 + N * 4 * A.natAbs ^ 2a:ℕS:ℕha:and✝.natAbs = 2 * (S + 1) + 1⊢ N * ((A.natAbs + S + 1) * (A.natAbs + S + 2)) = (N * A.natAbs + S + 1) * (N * A.natAbs + S + 2) nlinarith only [‹_› ▸ and]All goals completed! 🐙

  omegaAll goals completed! 🐙


-- TODO: also formalize the follow-up question:
-- “If $n$ and $k$ are fixed then can one say anything about the set of integers so represented?”

end Erdos686