Kolmogorov complexity and nondeterminism versus determinism for polynomial time computations

We call any consistent and sufficiently powerful formal theory that enables to algorithmically verify whether a text is a proof algorithmically verifiable mathematics (av-mathematics). We study the fundamental question whether nondeterminism is more powerful than determinism for polynomial time computations in the framework of av-mathematics. Our goal is to show strong indications that nondeterminism is more powerful than determinism for polynomial time computations. To do that, we do not consider decision problems only, but also compression algorithms. We show that at least one of the following three claims must be true: (i) [Formula presented] (ii) non-determinism is more powerful than determinism for polynomial-time compression (iii) for each polynomial-time compression algorithm there exists another one of the same asymptotic time complexity that compresses infinitely many strings logarithmically stronger Another surprising consequence of P = NP would be that time-bounded Kolmogorov complexity for any polynomial bound can be computed by deterministic algorithms in polynomial time.