lean_workbook_plus_60373

Proved

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

A pair of integers $(m,n)$ satisfies $m|n^2+1$ and $n|m^2+1$ . Prove that there are an infinite number of these pairs and describe a set of such pairs.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60373 (m n : ℤ) (h₁ : m ∣ n^2 + 1) (h₂ : n ∣ m^2 + 1) : ∃ m n, (m ∣ n^2 + 1 ∧ n ∣ m^2 + 1) ∧ (m > n)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph