lean_workbook_plus_78452

Proved

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

Prove that choosing any $n+1$ numbers from $1,2,..,2n$ there exist $2$ , $a$ and $b$ , so that $a|b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78452 (n : ℕ) (hn : 0 < n) (A : Finset ℕ) (hA : A.card = n + 1) (hA2 : ∀ a ∈ A, 0 < a ∧ a ≤ 2 * n) : ∃ a b, a ∈ A ∧ b ∈ A ∧ a ∣ b   :=  by sorry

Source

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

View graph