Set_of_Prime_Numbers_is_Primitive_Recursive

Proved

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

computabilityprime-numbersprimitive-recursive-functionsproofwiki

The set $\Bbb P$ of prime numbers is primitive recursive.

Preamble

import Mathlib.Computability.Primrec
import Mathlib.Data.Nat.Prime.Defs

Formal statement

theorem Set_of_Prime_Numbers_is_Primitive_Recursive : Nat.Primrec (fun n => if n.Prime then 1 else 0) := by sorry

Source