The exhaustive-search conjecture for proofs of Kolmogorov randomness

Let $R$ be the set of Kolmogorov-random strings, and let $t$ be a proof-length bound for statements asserting that no proof of $x\in R$ has length at most $t$. Exhaustive-search conjecture. Conditional program logic and case-based reasoning are typically useless for ruling out length-$t$ proofs that $x\in R$; consequently, the shortest proofs and fastest programs make no or limited use of such methods and rely primarily on exhaustive search. This is presented as a proposed explanation for the conjectured hardness of ruling out short proofs, not as an established consequence.