lean_workbook_plus_49351

Disproved

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

Prove that for all positive integers $n$ , there exist no integers $m$ such that $(2^{n}-1)(3^{n}-1)=m^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49351 : ∀ n : ℕ, ¬ (∃ m : ℤ, (2^n-1)*(3^n-1) = m^2)   :=  by sorry

Source