lean_workbook_plus_81229

Open

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

The Chan Shun Auditorium at UC Berkeley has room number $2050$ . The number of seats in the auditorium is a factor of the room number, and there are between $150$ and $431$ seats, inclusive. What is the sum of all of the possible numbers of seats in Chan Shun Auditorium?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81229 (n : ℕ) (h₁ : 150 ≤ n) (h₂ : n ≤ 431) (h₃ : n ∣ 2050) : ∑ k in Finset.filter (λ x => x ∣ 2050) (Finset.Icc 150 431), k = 615   :=  by sorry

Source

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

View graph