lean_workbook_plus_56540

Proved

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

Find the minimum possible value of $x^{2}+y^{2}$ given that $x$ and $y$ are real numbers satisfying: $xy(x^{2}-y^{2}) = x^{2} + y^{2}$ and $x$ does not equal 0.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56540 (x y : ℝ) (h₁ : x ≠ 0) (h₂ : x * y * (x^2 - y^2) = x^2 + y^2): x^2 + y^2 >= 0   :=  by sorry

Source

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

View graph