lean_workbook_plus_63237

Proved

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

Let the two positive numbers be $x$ and $y$ . Their product is $9$ so $xy = 9$ . According to the second condition, $1/x = 4(1/y)$ which implies $x = y/4$ . Putting that in the first equation, we get, $y^2 = 36$ so $y = 6$ and $x = 3/2$ so $x + y = 6 + 3/2 = 15/2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63237  (x y : ℝ)
  (h₀ : 0 < x ∧ 0 < y)
  (h₁ : x * y = 9)
  (h₂ : 1 / x = 4 * (1 / y)) :
  x + y = 15 / 2   :=  by sorry

Source

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

View graph