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 $\textbf{NP}$-intermediate -- the sparse complement of "$x{\in}R$ lacks a length $t$ proof" (where $R$'s complement is sparse) -- and has $\textbf{P/poly}$ circuits despite not being in $\textbf{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 $\textbf{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.

翻译：一种元复杂性假设——可行蔡廷不完全性（FCI）——断言排除长度为$t$的证明（证明字符串$x$具有柯尔莫哥洛夫随机性，例如$x{\in}R$）是困难的，这与蔡廷的结论（证明$x{\in}R$通常不可能）相类比。根据该假设，高效排除短证明需要（不可能地）排除任何证明。FCI具有强蕴涵：（i）随机选择的$x$通常会产生在任意给定证明系统中以高概率难以证明的重言式，密集地证伪其非最优性；（ii）在平均情形下无法证明$x{\in}R$，意味着在平均情形下证明重言式的困难性以及Feige猜想；（iii）一种自然语言是$\textbf{NP}$-中间者——"$x{\in}R$缺少长度为$t$的证明"的稀疏补集（其中$R$的补集是稀疏的）——且尽管不属于$\textbf{P}$，却拥有$\textbf{P/poly}$电路。FCI及其变体有力地断言：（i）不可计算性事实可转化为困难性猜想；（ii）众多开放复杂性问题具有预期答案（例如$\textbf{PH}$不坍塌），因此一个统摄性猜想可涵盖许多问题；（iii）某些不可证命题与难证命题之间存在同构映射。未来研究可将FCI与其他开放问题及困难性假设相关联；探讨$R$是否阻碍条件程序逻辑（从而蕴涵FCI）；并考虑扩展的同构映射是否将任何真的不可证命题映射至难证命题。