Given a formula $\phi$ of propositional logic, we define its size $|\phi|$ as the number of proposition symbols that $\phi$ contains (counted with multiplicity). For example, $|(p \land p)| = 2$.
Let $B_n$ denote the set of all Boolean functions $f:\{0,1\}^n \to \{0,1\}$ and $\Lambda$ and $\Gamma$ classes of boolean functions that are closed under subfunctions. We say that a property $\Phi: B_n \to \{0,1\}$ is a $\Gamma$-natural proof against $\Lambda$, if it satisfies the following conditions: (1) if $f \in \Lambda$, then $\Phi(f) = 0$ (2) $\Phi(f)$ for at least $2^{-O(n)}$ fraction of all $f\in B_n$ (3) $\Phi$ is in $\Gamma$.
Let $\mathrm{PolyF}$ denote the class of Boolean functions that can be computed by polynomial size formulas. Now, my question is the following: is it possible that there are, say, $\mathrm{P}/\mathrm{poly}$-natural proofs against $\mathrm{PolyF}$? Here by possible I mean that the existence of such a proof does not contradict some reasonable cryptographic assumption.
If $\mathrm{PolyF}$ contains pseudorandom number generators that are secure against $\mathrm{P}/\mathrm{poly}$-attacks, then it follows that there are no such proofs. Hence I'm potentially just asking whether this is indeed the case.
