A linear identity from two reciprocal quadratic constraints

Proved

WorkbookCorrected.plus_61420

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Let $x, y, z > 0$ : $xy+yz+zx = 1$ and $\frac{1}{1+x^2} + \frac{1}{1+y^2} = \frac{5}{1+z^2}$ . Prove that : $z = 2(x+y)$

Formalization Note: The original formalization added xyz=1, absent from the source and incompatible with xy+yz+zx=1 for positive variables. This corrected statement removes the added product assumption and proves the full source conclusion.

Source: InternLM Lean-Workbook, record lean_workbook_plus_61420 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.plus_61420 (x y z : ℝ) (hx : 0<x) (hy : 0<y) (hz : 0<z)
    (hxy : x*y+y*z+z*x=1)
    (h : 1/(1+x^2)+1/(1+y^2)=5/(1+z^2)) : z=2*(x+y) := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_61420; Apache-2.0

View graph