lean_workbook_plus_81137

Proved

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

We get that $5^{2m+3}=(3\times 5^m)^2+(4\times 5^m)^2+(10\times 5^m)^2$ and $5^{2m+4}= (12\times 5^m)^2+(15\times 5^m)^2+(16\times 5^m)^2$ for all $m\in \mathbb{Z}^+_0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81137 (m : ℕ) : (5^(2*m+3) = (3*5^m)^2 + (4*5^m)^2 + (10*5^m)^2) ∧ (5^(2*m+4) = (12*5^m)^2 + (15*5^m)^2 + (16*5^m)^2)   :=  by sorry

Source

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

View graph