lean_workbook_plus_35785

Proved

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

Correct solution: We'll first find the amount that's a multiple of $4$ or $6$ . From PIE, this is $250+166-83$ . Now we subtract off the amount that is a multiple of $24$ , or $41$ . This makes the answer $250+166-83-41 = \boxed{292}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35785 :
  Finset.card (Finset.filter (λ x => 4 ∣ x ∨ 6 ∣ x) (Finset.Icc 1 1000)) -
      Finset.card (Finset.filter (λ x => 24 ∣ x) (Finset.Icc 1 1000)) = 292   :=  by sorry

Source

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

View graph