lean_workbook_plus_45291

Disproved

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

The only positive integer solutions of the Diophantine equation $a^2 - 2b^4 = 1$ are $(a,b) = (1,1),(239,13)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45291 : { (a,b) : ℕ × ℕ | a^2 - 2*b^4 = 1} = {(1,1), (239,13)}   :=  by sorry

Source