Prove2Me

lean_workbook_plus_24513

Proved

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

Prove that if there exists a rational root of the equation 4x3−3x=p/q4x^3 - 3x = p/q where pp and qq are relatively prime integers, then qq must have a factor that is a perfect cube (not 1 or -1).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24513 (p q : ℤ) (hq : q ≠ 0) (hpq : Nat.Coprime p.natAbs q.natAbs) : (∃ x : ℚ, 4 * x ^ 3 - 3 * x = p / q) → ∃ y : ℤ, y ^ 3 ∣ q   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph