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 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 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 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 Not⊢ ∀ (n m : ℕ), m ≥ n + 2 → 4 ≠ ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1)))
  intro n m hmn:ℕm:ℕhm:m ≥ n + 2⊢ 4 ≠ ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1)))
  rw [ne_eq,n:ℕm:ℕhm:m ≥ n + 2⊢ ¬4 = ↑((m + 1) * (m + (1 + 1))) / ↑((n + 1) * (n + (1 + 1)))n:ℕm:ℕhm:m ≥ n + 2⊢ ¬4 * ↑((n + 1) * (n + (1 + 1))) = ↑((m + 1) * (m + (1 + 1))) eq_div_iff (byn:ℕm:ℕhm:m ≥ n + 2⊢ ↑((n + 1) * (n + (1 + 1))) ≠ 0n:ℕm:ℕhm:m ≥ n + 2⊢ ¬4 * ↑((n + 1) * (n + (1 + 1))) = ↑((m + 1) * (m + (1 + 1))) positivityAll goals completed! 🐙n:ℕm:ℕhm:m ≥ n + 2⊢ ¬4 * ↑((n + 1) * (n + (1 + 1))) = ↑((m + 1) * (m + (1 + 1))) : (↑((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))n:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2)⊢ False exact_mod_cast hn:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2)⊢ Falsen:ℕm:ℕhm:m ≥ n + 2h:4 * ((↑n + 1) * (↑n + 2)) = (↑m + 1) * (↑m + 2)h':4 * ((n + 1) * (n + 2)) = (m + 1) * (m + 2)⊢ False
  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)hc: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)hc:¬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)hc: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)hc:¬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 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 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⊢ ∃ 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⊢ 2 ≥ 2 validAll goals completed! 🐙
  field_simpx✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = N⊢ ∃ 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⊢ ∃ 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 = Nh:{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 = Nh:¬{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 = Nh:{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 = Nh:{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 = Nh:{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 = Nh:{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 = Nh:{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 = Nh:{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 = Nh:{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 _)x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = Nh:¬{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 = Nh:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ 0 < ?neg.convert_1✝
  show @@_ ↔ ¬ IsSquare (N * 4 : ℤ) → _x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = Nh:¬{n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty⊢ 0 < ↑N * 4
  ·x✝:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = Nh:¬{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 = Nh:¬{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 (byx✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 + 1) * (↑n + 2) ≠ 0x✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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) positivityAll goals completed! 🐙x✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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) : ((n : ℚ) + 1) * (↑n + 2) ≠ 0)] at heqx✝¹:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = Nh:¬{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 = Nh:¬{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⊢ ℤmpr.inlx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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)}.Nonemptympr.inrx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 * a + 1⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty ·x✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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⊢ ℤmpr.inlx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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)}.Nonemptympr.inrx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 * a + 1⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty boundAll goals completed! 🐙mpr.inlx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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)}.Nonemptympr.inrx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 * a + 1⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty : ℤ)).natAbs.even_or_oddmpr.inlx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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)}.Nonemptympr.inrx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 * a + 1⊢ {n | ∃ k, N * ((n + 1) * (n + 2)) = (k + 1) * (k + 2)}.Nonempty
    ·mpr.inlx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = Nh:¬{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_commx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = ?m.563All goals completed! 🐙]All goals completed! 🐙) |>.symm.trans (byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 [(byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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⊢ ?m.574All goals completed! 🐙 validAll goals completed! 🐙All goals completed! 🐙 :), sq,x✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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⊢ (l + l) * (l + l) = ?m.565All goals completed! 🐙 add_mulx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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⊢ l * (l + l) + l * (l + l) = ?m.565All goals completed! 🐙]All goals completed! 🐙))
        (byx✝²:TrueN:ℕhN_ge_2:N ≥ 2hN_not_square:¬IsSquare NhN_not_square':¬∃ s, s * s = Nh:¬{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 = Nh:¬{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 = Nh:¬{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 = Nh:¬{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