We study whether lower bounds against constant-depth algebraic circuits computing the Permanent over finite fields (Limaye–Srinivasan–Tavenas [J. ACM, 2025] and Forbes [CCC’24]) are hard to prove in certain proof systems. We focus on a DNF formula that expresses that such lower bounds are hard for constant-depth algebraic proofs. Using an adaptation of the diagonalization framework of Santhanam and Tzameret (SIAM J. Comput., 2025), we show unconditionally that this family of DNF formulas does not admit polynomial-size propositional AC$^0[p]$-Frege proofs, infinitely often. This rules out the possibility that the DNF family is easy, and establishes that its status is either that of a hard tautology for AC$^0[p]$-Frege or else unprovable (i.e., not a tautology). While it remains open whether the DNFs in question are tautologies, we provide evidence in this direction. In particular, under the plausible assumption that certain (weak) properties of multilinear algebra—specifically, those involving tensor rank—do not admit short constant-depth algebraic proofs, the DNFs are tautologies. We also observe that several weaker variants of the DNF formula are provably tautologies, and we show that the question of whether the DNFs are tautologies connects to conjectures of Razborov (ICALP’96) and Krajicek (J. Symb. Log., 2004). Additionally, our result has the following special features:

(i) *Existential depth amplification*: the DNF formula considered is parameterised by a constant depth d bounding the depth of the algebraic proofs. We show that there exists some fixed depth $d$ such that if there are no small depth-d algebraic proofs of certain circuit lower bounds for the Permanent, then there are no such small algebraic proofs in any constant depth.

(ii) *Necessity*: We show that our result is a necessary step towards establishing lower bounds against constant-depth algebraic proofs, and more generally against any sufficiently strong proof system. In particular, showing there are no short proofs for our DNF formulas, obtained by replacing ‘constant-depth algebraic circuits’ with any “reasonable” algebraic circuit class $C$, is necessary in order to prove any super-polynomial lower bounds against algebraic proofs operating with circuits from $C$.