Prove2Me

lean_workbook_plus_7009

Disproved

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

using sophie germain's identity \n 210+512=1254+4⋅44=(1252+2⋅42+2(5⋅4))(1252+2⋅42−2(5⋅4))=(16657)(14657) 2^{10} + 5^{12} = 125^{4} + 4\cdot4^{4} = (125^{2} + 2\cdot4^{2} + 2(5\cdot4))(125^{2} + 2\cdot4^{2} - 2(5\cdot4)) = (16657)(14657)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7009 :
  2^10 + 5^12 = 125^4 + 4 * 4^4 ∧
  125^4 + 4 * 4^4 = (125^2 + 2 * 4^2 + 2 * (5 * 4)) * (125^2 + 2 * 4^2 - 2 * (5 * 4))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph