lean_workbook_plus_49160

Disproved

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

Let $ax^3 = by^3 = cz^3$ and $\frac {1}{x} + \frac {1}{y} + \frac {1}{z} = 1$ . Prove that: $\boxed{\sqrt [3]{ax^2 + by^2 + cz^2} = \sqrt [3]{a} + \sqrt [3]{b} + \sqrt [3]{c}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49160 (a b c x y z : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hab : a * x ^ 3 = b * y ^ 3) (hbc : b * y ^ 3 = c * z ^ 3) (hxyz : 1 / x + 1 / y + 1 / z = 1) : (a * x ^ 2 + b * y ^ 2 + c * z ^ 2) ^ (1 / 3) = (a) ^ (1 / 3) + (b) ^ (1 / 3) + (c) ^ (1 / 3)   :=  by sorry

Source

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

View graph