Prove2Me

lean_workbook_plus_9866

Proved

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

8z3−6z+1  ⟹  4z3−3z=−128z^3-6z+1\implies 4z^3-3z=-\frac{1}{2} . Let z=cos⁡θz=\cos\theta and note the triple-angle formula cos⁡3θ=4cos⁡3θ−3cos⁡θ\cos 3\theta=4\cos^3\theta-3\cos\theta , you get cos⁡3θ=−12  ⟹  3θ=2πk±2π3=(6k±2)π3  ⟹  θ=(6k±2)π3\cos 3\theta=-\frac{1}{2}\implies 3\theta=2\pi k\pm\frac{2\pi}{3}=\frac{(6k\pm 2)\pi}{3}\implies\theta=\frac{(6k\pm 2)\pi}{3}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9866  (z : ℂ)
  (h₀ : 8 * z^3 - 6 * z + 1 = 0) :
  4 * z^3 - 3 * z = - 1 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph