Prove2Me

lean_workbook_plus_57818

Proved

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

Given a subset SS of {1,2,3,...,2n}\left\{1,2,3,...,2n\right\} with n+1n+1 elements, prove that there exist a,b∈Sa, b \in S such that a∣ba | b.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57818 (n : ℕ) (S : Finset ℕ) (hS : S ⊆ Finset.Icc 1 (2 * n)) (hS' : S.card = n + 1) : ∃ a b, a ∈ S ∧ b ∈ S ∧ a ∣ b   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph