Prove2Me

URM_Computable_Functions_of_One_Variable_is_Countably_Infinite

Proved

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

computabilityproofwikiurm-programs

The set U\mathbf U of all URM computable functions of 11 variable is countably infinite.

Preamble
import Mathlib.Computability.Partrec
Formal statement
theorem URM_Computable_Functions_of_One_Variable_is_Countably_Infinite : Countable {f : ℕ →. ℕ // Nat.Partrec f} := by sorry
Source
https://proofwiki.org/wiki/URM_Computable_Functions_of_One_Variable_is_Countably_Infinite

View graph