Advisor: Fabian Kunze
We present a formalization of Kolmogorov complexity and the non-random numbers in synthetic computability theory in the proof assistant Coq. In synthetic computability theory all functions $\mathbb{N} \rightarrow \mathbb{N}$ are considered computable and no external model of computation is required. The Kolmogorov complexity of an object is the size of its smallest description. A number whose Kolmogorov complexity is smaller than itself is defined as non-random or compressible.
We define Kolmogorov complexity in Coq using a universal interpreter and prove the invariance theorem. With the Berry paradox we prove the uncomputability of Kolmogorov complexity.
We formalize the many-one incompleteness of the non-random numbers. This is achieved by showing the simpleness of the non-random numbers. That means we show that the non-random numbers are enumerable, infinite and there exists no infinite, enumerable sub-predicate of the random numbers.
We mechanize Martin Kummer's proof of the existence of a minimal number of random numbers for every length. Additionally, Kummer proves the truth-table completeness of the non-random numbers. We give approaches to a potential formalization of this proof in Coq.
Except for Kummer's proof of the minimal count of random numbers, all of the major mechanized proofs use Markov’s principle and do not require excluded middle.