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.

## Error

Your reply will be screened

Your IP address will be recorded