Prove2Me

lean_workbook_plus_21837

Proved

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

Ok, now what about the sequence 11260,1840,1630,1504,1420,1360,1315,1280,1252\frac{1}{1260}, \frac{1}{840},\frac{1}{630},\frac{1}{504},\frac{1}{420},\frac{1}{360},\frac{1}{315},\frac{1}{280},\frac{1}{252} ?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21837 : ∃ a : ℕ → ℚ, a 0 = 1 / 1260 ∧ a 1 = 1 / 840 ∧ a 2 = 1 / 630 ∧ a 3 = 1 / 504 ∧ a 4 = 1 / 420 ∧ a 5 = 1 / 360 ∧ a 6 = 1 / 315 ∧ a 7 = 1 / 280 ∧ a 8 = 1 / 252   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph