lean_workbook_plus_26168

Proved

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

$3^{4^5}+4^{5^6} = \left(3^{4^4}\right)^4+4\left(2^{\frac{5^6-1}2}\right)^4 = x^4+4y^4$ where $x=3^{4^4}$ and $y=2^{\frac{5^6-1}2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26168 : 3^(4^5) + 4^(5^6) = (3^(4^4))^4 + 4 * (2^((5^6 - 1) / 2))^4   :=  by sorry

Source