lean_workbook_plus_53186

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $a$ , $b$ be integers greater than $2$ . Prove that there exists a positive integer $k$ and a finite sequence $n_1, n_2, . . . , n_k$ of positive integers such that $n_1=a$ , $n_k=b$ , and $n_{i}n_{i+1}$ is divisible by $n_i+n_{i+1}$ for each $i$ $(1\le i < k)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53186 (a b : ℤ) (hab : 2 < a ∧ 2 < b) :
    ∃ k : ℕ, ∃ n : ℕ → ℤ,
      n 0 = a ∧ n k = b ∧
      ∀ i, 0 < i ∧ i < k → (n i + n (i + 1)) ∣ n i * n (i + 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph