lean_workbook_plus_5016

Proved

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

Let $8x^3+1=3y$ . Hence, $y^3=6x-1$ and $8x^3-y^3=3y-6x$ , \nwhich gives $(2x-y)(4x^2+2xy+y^2+3)=0$ . Id est, $y=2x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5016  (x y : ℝ)
  (h₀ : 8 * x^3 + 1 = 3 * y)
  (h₁ : y^3 = 6 * x - 1) :
  8 * x^3 - y^3 = 3 * y - 6 * x → y = 2 * x   :=  by sorry

Source

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

View graph