lean_workbook_plus_52892

Proved

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

If $p$ and $q$ are two prime numbers, such that $q$ divides $q^2+1$ and $p$ divides $q^2-1$ . prove that $p+q+1$ is not a prime.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52892 (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (h : q ∣ q^2 + 1) (h' : p ∣ q^2 - 1) : ¬(p + q + 1).Prime   :=  by sorry

Source