If no optimal propositional proof system exists, we (and independently Pudlák) prove that ruling out length $t$ proofs of any unprovable sentence is hard. This mapping from unprovable to hard-to-prove sentences powerfully translates facts about noncomputability into complexity theory. For instance, because proving string $x$ is Kolmogorov random ($x{\in}R$) is ... more >>>

We consolidate two widely believed conjectures about tautologies---no optimal proof system exists, and most require superpolynomial size proofs in any system---into a $p$-isomorphism-invariant condition satisfied by all paddable $\textbf{coNP}$-complete languages or none. The condition is: for any Turing machine (TM) $M$ accepting the language, $\textbf{P}$-uniform input families requiring superpolynomial time ... more >>>

Informally, a language L has speedup if, for any Turing machine for L, there exists one that is better. Blum showed that there are computable languages that have almost-everywhere speedup. These languages were unnatural in that they were constructed for the sole purpose of having such speedup. We identify a ... more >>>