Are there proofs with (say) n^2 symbols, in a proof system of your choice, for which (a) there exist proofs of the same statements with n symbols, but (b) finding the shorter proofs is computationally intractable?
Let's say our proof system has axiom-schema:
A1. M * N + R = T for all valid combinations of integers with 0 <= R < N
A2. SHA( K ) = N for all valid integers such that SHA-256 applied to the binary representation of K results in the binary representation of N
As well as inference rules
I1. NO_DIVISORS_UP_TO( P, 2 ) if M * 2 + 1 = P for some M
I2. NO_DIVISORS_UP_TO( P, K ) if NO_DIVISORS_UP_TO( P, K - 1 ) and M * K + R = P for some M, R != 0
I3. ODD_PRIME( P ) if NO_DIVISORS_UP_TO( P, P - 1 )
I4. ODD_PRIME( P ) if NO_DIVISORS_UP_TO( P, S + 1 ) and S * S + R = P for some S, R != 0 and SHA( K ) = P for some K
In this system a proof of ODD_PRIME( P ) takes about 2P steps if we use inference rule I3, for example:
5 * 2 + 1 = 11 [A1] NO_DIVISORS_UP_TO( 11, 2 ) [I1] 3 * 3 + 2 = 11 [A1] NO_DIVISORS_UP_TO( 11, 3 ) [I2] 2 * 4 + 3 = 11 [A1] NO_DIVISORS_UP_TO( 11, 4 ) [I2] 2 * 5 + 1 = 11 NO_DIVISORS_UP_TO( 11, 5 ) 1 * 6 + 5 = 11 NO_DIVISORS_UP_TO( 11, 6 ) 1 * 7 + 4 = 11 NO_DIVISORS_UP_TO( 11, 7 ) ... 1 * 10 + 1 = 11 [A1] NO_DIVISORS_UP_TO( 11, 10 ) [I2] ODD_PRIME( 11 ) [I3]
But only about 2*sqrt(P) steps if we use inference rule I4. But in order to introduce the necessary axiom using A2 we have to perform a computationally intractable amount of work to identify K.
I think, however, that Dr. Aaronson was actually looking for propositional proof systems that can prove any tautology in classical logic--- a much more difficult exercise than my toy language here. However, the same sort of embedding might be feasible.