lean_workbook_plus_12909

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_12909 (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (h : q ∣ q^2 + 1) (h' : p ∣ q^2 - 1) : ¬(Nat.Prime (p + q + 1))   :=  by sorry

Source

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

View graph