2 z^6 - 3 α z^4 - 2 β z^3 + 3 α^2 z^2 + β^2 - α^3 = 0

The equation can be rewritten as a quadratic in β. After completing the square one obtains the equivalent condition \[(β−z^3)^2+(z^2−α)^3=0.\] Since the first term is a square, it is non‑negative, so the second term must be non‑positive. This forces α≥z². With this inequality the equation becomes \[(β−z^3)^2=(α−z^2)^3,\] and taking square roots gives the two real solutions \[\beta=z^3\pm(α−z^2)\sqrt{α−z^2}.\] Thus the set of all real solutions of the original equation is exactly the set of triples (α,β,z) with α≥z² and β equal to one of the two expressions above. The two families are exhaustive because any solution must satisfy the derived quadratic, and the discriminant analysis shows that no other real solutions exist.

The given polynomial can be rewritten as a sum of a square and a cube. Expanding the right‑hand side and simplifying with the `ring` tactic shows that \[ 2z^6-3\alpha z^4-2\beta z^3+3\alpha^2 z^2+\beta^2-\alpha^3 = (\beta-z^3)^2+(z^2-\alpha)^3. \] Hence the equation `eq4 α β z = 0` is equivalent to \[ (\beta-z^3)^2+(z^2-\alpha)^3 = 0. \] The Lean lemma below formalises this equivalence. It unfolds the definition of `eq4`, proves the algebraic identity with `ring`, and then uses `simpa` to rewrite the goal in either direction.

The given polynomial can be rewritten as a sum of a perfect cube and a perfect square. Indeed, expanding the right‑hand side of the identity \[(z^2-\alpha)^3+(z^3-\beta)^2\] yields exactly the left‑hand side of the equation. Consequently the equation \[ 2 z^6-3\alpha z^4-2\beta z^3+3\alpha^2 z^2+\beta^2-\alpha^3=0 \] is equivalent to \[ (z^2-\alpha)^3+(z^3-\beta)^2=0. \] For real numbers a sum of a square and a cube can vanish only when the cube is non‑positive and the square is the negative of that cube. Setting \(t=\alpha-z^2\) we obtain \(t\ge0\) and \((z^3-\beta)^2=t^3\). Hence there exists a real number \(s\) with \(s^2=t^3\) and \(\beta=z^3+s\). Conversely, any choice of real \(z\), non‑negative \(t\) and \(s\) with \(s^2=t^3\) gives a triple \((\alpha,\beta,z)\) with \(\alpha=z^2+t\) and \(\beta=z^3+s\) that satisfies the original equation. Thus the complete solution set is \[ \{(\alpha,\beta,z)\in\mathbb R^3\mid \exists\,t\ge0,\ \exists\,s,\ s^2=t^3,\ \alpha=z^2+t,\ \beta=z^3+s\}. \] The factorisation above is proved formally in Lean by a simple ring calculation.

We consider the equation \[ 2z^6-3\alpha z^4-2\beta z^3+3\alpha^2 z^2+\beta^2-\alpha^3=0, \] as a quadratic in the variable \(\beta\). Rearranging gives \[ \beta^2-2z^3\beta+\bigl(2z^6-3\alpha z^4+3\alpha^2z^2-\alpha^3\bigr)=0 . \] The discriminant of this quadratic is \[ \Delta=(2z^3)^2-4\bigl(2z^6-3\alpha z^4+3\alpha^2z^2-\alpha^3\bigr) =4(\alpha-z^2)^3 . \] Hence \(\Delta\ge0\) iff \(\alpha\ge z^2\). When \(\alpha\ge z^2\) we can write \(\alpha-z^2=t^2\) for some \(t\ge0\). Then \(\sqrt{\Delta}=2t^3\) and the two roots are \[ \beta=z^3\pm t^3 . \] Thus every real solution of the equation is of the form \[ \alpha=z^2+t^2,\qquad \beta=z^3\pm t^3\qquad(t\ge0). \] Conversely, substituting these expressions into the left‑hand side of the equation and simplifying by the ring tactic shows that the identity holds identically. Consequently the set of all real solutions is exactly the two one‑parameter families described above. Below is a Lean 4 fragment that formalises the “forward” direction: for any \(t\ge0\) the pair \((\alpha,\beta)\) defined by the formulas above satisfies the equation. The proof uses only the definition of `eq4`, the rewriting rules for the parameters, and the `ring` tactic to finish the algebraic simplification. --- ```lean -- Definition of the solution family def Sol (α β z : ℝ) : Prop := ∃ t : ℝ, 0 ≤ t ∧ α = z ^ 2 + t ^ 2 ∧ (β = z ^ 3 + t ^ 3 ∨ β = z ^ 3 - t ^ 3) -- Theorem: every member of the family satisfies the equation theorem eq4_sound (α β z : ℝ) (h : Sol α β z) : eq4 α β z := by rcases h with ⟨t, ht, hα, hβ⟩ rcases hβ with hβpos | hβneg · -- β = z^3 + t^3 have : eq4 α β z := by simp [eq4, hα, hβpos] ring exact this · -- β = z^3 - t^3 have : eq4 α β z := by simp [eq4, hα, hβneg] ring exact this ``` The `simp` step rewrites the goal using the definitions of `α` and `β`; the remaining equality is a purely algebraic identity, which the `ring` tactic verifies automatically. This completes the formal proof that the two families indeed solve the equation.

-- Lean-формализация постановки eq4.
-- Окружение: Lean 4 + Mathlib (версия 27), без `import` (Mathlib предзагружен).
-- Имена переменных и сигнатура `def eq4` ФИКСИРОВАНЫ — менять нельзя.

def eq4 (α β z : ℝ) : Prop :=
  2 * z ^ 6 - 3 * α * z ^ 4 - 2 * β * z ^ 3 + 3 * α ^ 2 * z ^ 2 + β ^ 2 - α ^ 3 = 0


def Sol (α β z : ℝ) : Prop :=
  ∃ t : ℝ, 0 ≤ t ∧ α = z ^ 2 + t ^ 2 ∧ (β = z ^ 3 + t ^ 3 ∨ β = z ^ 3 - t ^ 3)


theorem eq4_sound (α β z : ℝ) (h : Sol α β z) : eq4 α β z :=
by
  rcases h with ⟨t, ht, hα, hβ⟩
  rcases hβ with hβpos | hβneg
  · -- β = z^3 + t^3
    have : eq4 α β z := by
      simp [eq4, hα, hβpos]
      ring
    exact this
  · -- β = z^3 - t^3
    have : eq4 α β z := by
      simp [eq4, hα, hβneg]
      ring
    exact this

The key observation is that the left‑hand side of the equation can be rewritten as a sum of a square and a cube. Expanding \((\beta-z^3)^2\) and \((z^2-\alpha)^3\) gives exactly the polynomial in the definition of `eq4`. Hence \[ 2z^6-3\alpha z^4-2\beta z^3+3\alpha^2 z^2+\beta^2-\alpha^3 =(\beta-z^3)^2+(z^2-\alpha)^3 . \] Consequently the equation `eq4 α β z` is equivalent to the simpler condition \[ (\beta-z^3)^2+(z^2-\alpha)^3=0 . \] This form immediately yields a parametrisation: for any real numbers \(z,u\) set \[ \alpha=z^2+u^2,\qquad \beta=z^3+u^3 . \] Then \(\alpha-z^2=u^2\) and \(\beta-z^3=u^3\), so the square and the cube are both \(u^6\) and the equation is satisfied. The converse also holds in an algebraically closed field: if the square‑plus‑cube equation holds, the two terms have a common sixth‑root \(u\), and the above formulas recover \(\alpha,\beta\). Thus the parametric family \((\alpha,\beta,z)=(z^2+u^2,\;z^3+u^3,\;z)\) describes all solutions. Finally, the factorisation \[ z^6-y^3=(z^2-y)(z^4+z^2y+y^2) \] follows from the identity \(a^3-b^3=(a-b)(a^2+ab+b^2)\) with \(a=z^2,\;b=y\). All these identities are verified in Lean by a single `ring` tactic.

def eq4 (α β z : ℝ) : Prop :=
  2 * z ^ 6 - 3 * α * z ^ 4 - 2 * β * z ^ 3 + 3 * α ^ 2 * z ^ 2 + β ^ 2 - α ^ 3 = 0

lemma eq4_eq_square_plus_cube (α β z : ℝ) :
  2 * z ^ 6 - 3 * α * z ^ 4 - 2 * β * z ^ 3 + 3 * α ^ 2 * z ^ 2 + β ^ 2 - α ^ 3 =
    (β - z ^ 3) ^ 2 + (z ^ 2 - α) ^ 3 := by
  ring

lemma eq4_iff_square_plus_cube (α β z : ℝ) :
  eq4 α β z ↔ (β - z ^ 3) ^ 2 + (z ^ 2 - α) ^ 3 = 0 := by
  unfold eq4
  have h :
    2 * z ^ 6 - 3 * α * z ^ 4 - 2 * β * z ^ 3 + 3 * α ^ 2 * z ^ 2 + β ^ 2 - α ^ 3 =
      (β - z ^ 3) ^ 2 + (z ^ 2 - α) ^ 3 := by
    ring
  simpa [h]

lemma implies_cubic_square (α β z : ℝ) (h : (α - z ^ 2) ^ 3 = (β - z ^ 3) ^ 2) :
  (α - z ^ 2) ^ 3 = (β - z ^ 3) ^ 2 := h

lemma eq4_param (z u : ℝ) : eq4 (z ^ 2 + u ^ 2) (z ^ 3 + u ^ 3) z := by
  unfold eq4
  ring

lemma factorization_eq (z y : ℝ) :
  z ^ 6 - y ^ 3 = (z ^ 2 - y) * (z ^ 4 + z ^ 2 * y + y ^ 2) := by
  ring

The polynomial in the equation can be rewritten by a simple algebraic manipulation. Expanding the cube \((z^2-\alpha)^3\) and the square \((z^3-\beta)^2\) gives \[(z^2-\alpha)^3+(z^3-\beta)^2 = z^6-3\alpha z^4+3\alpha^2 z^2-\alpha^3+z^6-2\beta z^3+\beta^2 = 2z^6-3\alpha z^4-2\beta z^3+3\alpha^2 z^2+\beta^2-\alpha^3. \] Thus the original equation is equivalent to the sum of a cube and a square being zero: \[(z^2-\alpha)^3+(z^3-\beta)^2=0. \] Because a square is always non‑negative, the only way the sum can vanish is that the cube is non‑positive and its magnitude equals the square. Hence we must have \[(z^2-\alpha)\le 0\quad\text{and}\quad (z^3-\beta)^2=-(z^2-\alpha)^3. \] The first inequality is equivalent to \(\alpha\ge z^2\). The second equation gives two possible values for \(\beta\): \[\beta=z^3\pm\sqrt{-(z^2-\alpha)^3}. \] Consequently the complete set of real solutions of the equation is \[\{(\alpha,\beta,z)\in\mathbb R^3\mid \alpha\ge z^2\ \text{and}\ \beta=z^3\pm\sqrt{-(z^2-\alpha)^3}\}. \] The special case \(\alpha=z^2\) yields \(\beta=z^3\) and gives the trivial family of solutions. For every \(\alpha>z^2\) the two signs produce distinct solutions, and together these families exhaust all possibilities, proving the completeness of the description. The Lean fragment below formalises the key algebraic identity that underlies the whole argument.

The equation in the statement can be rewritten as a difference of a square and a cube. Expanding \((β - z^3)^2\) gives \(β^2 - 2βz^3 + z^6\) and expanding \((α - z^2)^3\) gives \(α^3 - 3α^2z^2 + 3αz^4 - z^6\). Subtracting the latter from the former yields exactly the left‑hand side of the original equation. Hence the equation is equivalent to \((β - z^3)^2 = (α - z^2)^3\). In Lean we formalise this by proving an equivalence lemma `eq4_iff`. We first unfold the definition of `eq4`, then use the `ring` tactic to establish the algebraic identity between the two expressions. The forward direction rewrites the hypothesis using this identity to obtain a statement of the form `a - b = 0`, from which `sub_eq_zero.mp` gives `a = b`. The reverse direction starts from `a = b`, turns it into `a - b = 0` with `sub_eq_zero.mpr`, and rewrites back to the original form with the same `ring` identity. This completes the proof that the set of solutions of `eq4` is exactly the set of triples \((α,β,z)\) satisfying \((β - z^3)^2 = (α - z^2)^3\).

We prove the familiar algebraic identity for real numbers: for all real \(x\) and \(y\), \((x+y)^2 = x^2 + 2xy + y^2\). In Lean, this follows immediately from the `ring` tactic, which normalises polynomial expressions over a commutative ring. The theorem is stated for the type `ℝ` and the proof is a one‑liner invoking `ring`. The Lean code below is self‑contained (no explicit imports are required because the standard Mathlib environment is preloaded).

theorem sq_add_sq (x y : ℝ) : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
  ring

We first observe that the polynomial in the definition of `eq4` can be rewritten in a factorised form. Expanding the cube \((α−z^2)^3\) and the square \((z^3−β)^2\) gives \[(α−z^2)^3 = α^3−3α^2z^2+3αz^4−z^6,\qquad (z^3−β)^2 = z^6−2βz^3+β^2.\] Subtracting the second expression from the first and multiplying by \(-1\) yields exactly the left‑hand side of `eq4`. Hence \[\eq4 α β z \iff -( (α−z^2)^3−(z^3−β)^2)=0 \iff (α−z^2)^3−(z^3−β)^2=0 \iff (α−z^2)^3=(z^3−β)^2.\] This identity gives a complete description of the solution set: for any real numbers \(α,β,z\) the equation holds precisely when the cube of \(α−z^2\) equals the square of \(z^3−β\). Equivalently, \(α=z^2+|z^3−β|^{2/3}\). The proof in Lean follows the same algebraic manipulation, using the `ring` tactic to normalise the polynomial and the lemmas `neg_eq_zero` and `sub_eq_zero` to convert the zero‑condition into an equality. Consequently, the family of solutions described by the equality \((α−z^2)^3=(z^3−β)^2\) is exhaustive: every triple \((α,β,z)\) satisfying the original equation belongs to this family, and every triple in the family satisfies the equation. The Lean code below formalises this equivalence.