lean_workbook_plus_43171

Open

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

There are $1469$ numbers in $\{1,...,2004\}$ which are divisible by at least one of 2,3 and 5

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43171 : ∑ k in Finset.filter (λ x => 2∣x ∨ 3∣x ∨ 5∣x) (Finset.Icc 1 2004), 1 = 1469   :=  by sorry

Source