lean_workbook_plus_55079

Proved

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

$k=3m$ . we have $m(12m-1)=y^{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55079 {k m y : ℤ} (h₁ : k = 3*m) (h₂ : m*(12*m - 1) = y^2) : ∃ k m y : ℤ, k = 3*m ∧ m*(12*m - 1) = y^2   :=  by sorry

Source