Prove2Me

lean_workbook_plus_66779

Disproved

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

If y≠0y \neq 0, then: 72x3+4xy2=11y3⇔72(xy)3+4xy−11=072x^3 + 4xy^2 = 11y^3 \Leftrightarrow 72\left( \frac {x}{y}\right)^3 + 4\frac {x}{y} - 11 = 0; and if: xy=t\frac {x}{y} = t, 72t3+4t−11=072t^3 + 4t - 11 = 0 and t=12t = \frac {1}{2} solution ⇒x=2y\Rightarrow x = 2y.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66779  (x y : ℝ)
  (h₀ : y ≠ 0)
  (h₁ : 72 * x^3 + 4 * x * y^2 = 11 * y^3) :
  72 * (x / y)^3 + 4 * (x / y) - 11 = 0 ∧ x = 2 * y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph