lean_workbook_plus_28398

Proved

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

Prove that there are no positive integer solutions for $m$ and $n$ in the equation $2^m + 3 = 11^n$ when $m \ge 4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28398 (m n : ℕ) (h₁ : 2 ^ m + 3 = 11 ^ n) (h₂ : 4 ≤ m) : ¬ (0 < m ∧ 0 < n)   :=  by sorry

Source