lean_workbook_plus_24343

Proved

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

Given a set A of finitely many primes. Prove that there are only finitely many $n$ such that any prime dividing $n$ or $n+1$ belongs to A.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24343 (A : Finset ℕ) (hA : ∀ a ∈ A, a.Prime) : {n : ℕ | ∀ p : ℕ, p ∣ n ∨ p ∣ n + 1 → p ∈ A}.Finite   :=  by sorry

Source