Trustworthy Systems

On the formalisation of kolmogorov complexity


Elliot Catt and Michael Norrish


Australian National University


Kolmogorov complexity is an essential tool in the study of algorithmic information theory, and is used in the fields of Artificial Intelligence, cryptography, and coding theory. The formalisation of the theorems of Kolmogorov complexity is also key to proving results in the theory of Intelligent Agents, specifically the results in Universal Artificial Intelligence. In this paper, we present a mechanisation of some of these fundamental results. In particular, building on HOL4's existing model of computability, we provide a formal definition of the complexity of a binary string, and then prove (i) that Kolmogorov complexity is uncomputable; (ii) the Kolmogorov Complexity invariance theorem; (iii) the Kraft and Kolmogorov-Kraft inequalities; and (iv) key Kolmogorov Complexity inequalities.

BibTeX Entry

    address          = {Online},
    author           = {Catt, Elliot and Norrish, Michael},
    booktitle        = {Certified Proofs and Programs},
    date             = {2021-1-17},
    doi              = {},
    month            = jan,
    pages            = {291--299},
    publisher        = {ACM},
    title            = {On the Formalisation of Kolmogorov Complexity},
    volume           = {online in press},
    year             = {2021}