lean_workbook_plus_29389

Proved

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

Let $m$ be a fixed positive integer. Prove that there exists infinitely many pairs of positive integers $(a,b)$ st $a | b^2 + m$ and $b | a^2 + m$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29389 (m : ℕ) (hm : 0 < m) : ∃ a b : ℕ, a ∣ b^2 + m ∧ b ∣ a^2 + m   :=  by sorry

Source