lean_workbook_plus_54500

Proved

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

Let $ab=t^2$ then we have $\sqrt{t^4+b^4}=2kb$ so $t^4+b^4=4k^2b^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54500  (a b t k : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < t ∧ 0 < k)
  (h₁ : a * b = t^2)
  (h₂ : Real.sqrt (t^4 + b^4) = 2 * k * b) :
  t^4 + b^4 = 4 * k^2 * b^2   :=  by sorry

Source

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

View graph