lean_workbook_plus_31840

Proved

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

Prove that there are no positive integers x and y such that $7^{x}-1=12(2y+1)^{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31840 (x y : ℕ) (h₁ : 0 < x ∧ 0 < y) (h₂ : 7^x - 1 = 12 * (2 * y + 1)^2) : False   :=  by sorry

Source