lean_workbook_plus_9744

Proved

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

Given 16 distinct positive integers not exceeding 100, prove that it is possible to choose 4 distinct integers $a$ , $b$ , $c$ and $d$ such that $a+c = b + d$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9744 (A : Finset ℕ) (hA : A.card = 16) (hA' : ∀ 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