# A Formalization of Kolmogorov Complexity in Synthetic Computability Theory

## Abstract

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.

## Main References

• Andrei N. Kolmogorov. “Three approaches to the quantitative definition of information”. In: Problems of information transmission 1.1 (1965).
• Alexander K. Zvonkin and Leonid A. Levin. “The complexity of finite objects and the development of the concepts of information and randomness by means of the theory of algorithms”. In: Russian Mathematical Surveys 25.6 (1970).
• Martin Kummer. “On the complexity of random strings”. In: Annual Symposium on Theoretical Aspects of Computer Science. Springer. 1996.
• Yannick Forster. “Computability in Constructive Type Theory”. PhD thesis. Saarland University, 2021.