Razborov and Rudich's paper

Natural Proofs
gives a combinatorial framework for proofs to show that circuits in
a given class cannot achieve a given computational task. The paper
explains the difficultly of extending these proofs to show, for
example, that NP does not have polynomial-size circuits (and thus
P≠NP). But do natural proofs really present a barrier to proving
important circuit lower bounds?

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.

Razborov and Rudich show that such a proof against polynomial-size
circuits would break pseudorandom generators and in particular imply that
the discrete logarithm is not hard. So under reasonable hardness
assumptions, natural proofs cannot be used to prove lower bounds
against polynomial-size circuits. See the

paper for more
details.

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 C_{n} 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

If C is constructive then Discrete logarithm is easy
which is just a "pigs can fly" theorem that we see often in
complexity.

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.