Prove2Me

lean_workbook_plus_62794

Proved

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

Compute 2000×2007×2008×2015+784\sqrt{2000 \times {2007} \times {2008} \times {2015}+784}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62794 (x : ℕ) : √(2000 * 2007 * 2008 * 2015 + 784) = 4030028   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph