One approach to showing NP does not have polynomial-size circuits: Find some property C of functions such that SAT is in C. We then show, using some sort of inductive argument, that no function computable by polynomial-size circuits can have property C. This would imply SAT, cannot have polynomial-size circuits.
Briefly a natural proof is such a proof where C has two properties.
- Largeness: C contains many functions.
- Constructivity: One can efficiently verify that a function f is in C.
Sounds bad for proofs against circuits. But let's consider the two properties. The authors give a good argument why the largeness condition should hold, however
We do not have any similar formal evidence for constructivity, but from experience it is plausible to say that we do not yet understand the mathematics of Cn outside exponential time (as a function of n) well enough to use them effectively in a combinatorial style proof. We make this point in Section 3, where we argue that all known lower bound proofs against nonmonotone circuits are natural by our definition.Indeed they do show all known proofs are natural, but in some cases go through considerable effort to "naturalize" these proofs (as opposed to relativization where the fact that a theorem relativizes follows immediately from the proof).
Consider what I call quasinatural proofs, where we only require the largeness condition. One might say that if discrete logarithm is hard then a quasinatural proof must prove the nonconstructivity of C. But really you get a conditional. If there are quasinatural proofs against polynomial-size circuits then
Avi Wigderson points out that unconditionally you cannot have a natural proof showing that the discrete logarithm problem is hard. If we unravel this statement then we get that giving a quasinatural proof showing discrete logarithm is hard would require proving that discrete logarithm is hard, hardly a surprise.
I don't have an example of a quasinatural proof not known to be natural as we have very limited techniques for proving circuit lower bounds. Natural proofs do give us some insight into what kind of proof techniques we need for stronger lower bounds, but they do not, in and of themselves, present a major barrier to finding such proofs.