lean_workbook_plus_34880

Proved

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

Prove that in a subset $S$ of the set $A=\{1,2,...,4s-1,4s\}$ with size $2s+2$ , we can find three distinct numbers $x$ , $y$ , and $z$ such that $x+y=2z$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34880 (s : ℕ) (hs : s > 0) (A : Finset ℕ) (hA : A = Finset.Icc 1 (4 * s)) (hA' : A.card = 2 * s + 2) : ∃ x y z : ℕ, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x ≠ y ∧ y ≠ z ∧ x ≠ z ∧ x + y = 2 * z   :=  by sorry

Source

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

View graph