Hardness of Ruling Out Short Proofs of Kolmogorov Randomness

A meta-complexity assumption, Feasible Chaitin Incompleteness (FCI), asserts the hardness of ruling out length $t$ proofs that string $x$ is Kolmogorov random (e.g. $x\in R$), by analogy to Chaitin’s result that proving $x\in R$ is typically impossible. By assertion, efficiently ruling out short proofs requires, impossibly, ruling out any proof. FCI has strong implications: (i) randomly chosen $x$ typically yields tautologies hard with high probability for any given proof system, densely witnessing its nonoptimality; (ii) average-case impossibility of proving $x\in R$ implies average-case hardness of proving tautologies and Feige’s hypothesis; and (iii) a natural language is $\mathbf{\text{NP}}$-intermediate – the sparse complement of “$x\in R$ lacks a length $t$ proof” (where $R$’s complement is sparse) – and has $\mathbf{\text{P/poly}}$ circuits despite not being in $\mathbf{\text{P}}$. FCI and its variants powerfully assert: (i) noncomputability facts translate to hardness conjectures; (ii) numerous open complexity questions have the expected answers (e.g. non-collapse of $\mathbf{\text{PH}}$), so one overarching conjecture subsumes many questions; and (iii) an implicit mapping between certain unprovable and hard-to-prove sentences is an isomorphism. Further research could relate FCI to other open questions and hardness hypotheses; consider whether $R$ frustrates conditional program logic, implying FCI; and consider whether an extended isomorphism maps any true unprovable sentence to hard-to-prove sentences.