Not_All_Natural_Number_Functions_are_Primitive_Recursive
Provedcomputabilityprimitive-recursive-functionsproofwiki
Not all functions are primitive recursive.
Preamble
import Mathlib.Computability.Primrec
Formal statement
theorem Not_All_Natural_Number_Functions_are_Primitive_Recursive : ∃ (f : ℕ → ℕ), ¬Nat.Primrec f := by sorry
Source