lean_workbook_plus_44767

Proved

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

Multiplying both sides by $4(ab)^2$ we get $(16-b^2)(a^2+2a-1)+(16-a^2)(b^2+2b-1)=168$ , which quickly leads to $17(a^2+b^2)+24(a+b)-232=0.$ Now set $t=a+b>0$ , and thus $t^2-8=a^2+b^2,$ and get $17t^2+24t-368=0$ , which has as solutions $t_1=4$ and $t_2=-92/17,$ with the latter not being acceptable. So, we have $a+b=4$ and $ab=4$ , and therefore $a=b=2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44767  (a b : ℝ)
  (h₀ : 0 < a ∧ 0 < b)
  (h₁ : a * b = 4)
  (h₂ : a + b = 4) :
  a = 2 ∧ b = 2   :=  by sorry

Source

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

View graph