lean_workbook_plus_35307

Proved

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

Let $x,y>0$ and $(x+y+1)xy=x^2+y^2$ . Find the maximum value of $P=\frac{1}{x^3}+\frac{1}{y^3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35307 (x y P : ℝ) (hx : 0 < x) (hy : 0 < y) (hP: P = 1/x^3 + 1/y^3) (h : (x + y + 1) * x * y = x^2 + y^2) : P <= 16   :=  by sorry

Source

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

View graph