lean_workbook_plus_75865

Disproved

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

The equation $2^{x} -1 = 7^{y}$ has only one root in $\mathbb{N}$ ; that is $(x;y) = (3;1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75865 : { (x,y) : ℕ × ℕ | 2^x - 1 = 7^y} = { (3,1) }   :=  by sorry

Source