lean_workbook_plus_11795

Disproved

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

Show that $2005^{1002^2} \cdot (41^2 + 18^2) = 2005^{2005}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11795 : 2005^(1002^2) * (41^2 + 18^2) = 2005^(2005)   :=  by sorry

Source