lean_workbook_plus_75262

Proved

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

Prove that among 16 different positive integers less than or equal to 100, we have positive integers $a,b,c,d$ such that $a+c=b+d$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75262 (A : Finset ℕ) (hA : A.card = 16) (hA2: ∀ a ∈ A, a ≤ 100) : ∃ a b c d : ℕ, a ∈ A ∧ b ∈ A ∧ c ∈ A ∧ d ∈ A ∧ a + c = b + d   :=  by sorry

Source

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

View graph