Prove2Me

lean_workbook_plus_50001

Disproved

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

so S =(24−1)+2(34−24)+3(44−34)+4(54−44)+5(64−54)+6(2006−64) =(2^4-1)+2(3^4-2^4)+3(4^4-3^4)+4(5^4-4^4)+5(6^4-5^4)+6(2006-6^4) S=9781 S=9781

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50001  (s : ℝ)
  (h₀ : s = (2^4 - 1) + 2 * (3^4 - 2^4) + 3 * (4^4 - 3^4) + 4 * (5^4 - 4^4) + 5 * (6^4 - 5^4) + 6 * (2006 - 6^4)) :
  s = 9781   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph