Introduction to Computability Theory in Lean (Part 1)
Published:
🚧 Under construction
This post series will cover computability theory in Lean.
It will include introductions to and formalizations of:
- oracle-relative computation via partial recursive functions,
- reducibility,
- the jump operator,
- and the arithmetic hierarchy
- Turing degrees and their structure