lean_workbook_plus_43751

Proved

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

Prove that for any integer $n\ge2$ , there exist positive integer $a_1,a_2,...,a_n$ such that $a_j-a_i$ divides $a_j+a_i$ for $1\le i<j\le n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43751 (n : ℕ) (_hn : 2 ≤ n) :
    ∃ a : ℕ → ℕ,
      ∀ i j : ℕ,
        i < j →
          i ≤ n ∧
            j ≤ n →
              (a j - a i) ∣ (a j + a i)   :=  by sorry

Source

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

View graph