Document Open Access Logo

AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard

Authors Jiaqi Lu , Rahul Santhanam , Iddo Tzameret

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITCS.2026.99.pdf
  • Filesize: 0.99 MB
  • 25 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Proof theory
  • Theory of computation → Algebraic complexity theory
Keywords
  • Complexity
  • Lower bounds
  • Proof complexity
  • AC⁰[p]-Frege
  • Diagonalisation
  • Algebraic complexity

Metrics

Abstract

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⁰[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⁰[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 Krajíček (J. Symb. Log., 2004). 

Additionally, our result has the following special features:  
ii) 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. 
iii) 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.

Cite As Get BibTex

Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 99:1-99:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITCS.2026.99

Author Details

Jiaqi Lu
  • Department of Computing, Imperial College London, UK
Rahul Santhanam
  • Department of Computer Science, Oxford University, UK
Iddo Tzameret
  • Department of Computing, Imperial College London, UK

Funding

  • Lu, Jiaqi: This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 101002742, EPRICOT project).
  • Santhanam, Rahul: This project was partly funded by the EPSRC grant EP/Z534158/1, Integrated Approach to Computational Complexity: Structure, Self-Reference and Lower Bounds.
  • Tzameret, Iddo: This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 101002742, EPRICOT project). It was also supported by the Engineering and Physical Sciences Research Council (EPSRC) under grant EP/Z534158/1, Integrated Approach to Computational Complexity: Structure, Self-Reference and Lower Bounds.

References

  1. Miklós Ajtai. The complexity of the pigeonhole principle. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science, pages 346-355, 1988. URL: https://doi.org/10.1109/SFCS.1988.21951.
  2. Miklós Ajtai. The independence of the modulo p counting principles. In Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, pages 402-411, 1994. Google Scholar
  3. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Pseudorandom generators in propositional proof complexity. SIAM J. Comput., 34(1):67-88, 2004. (A preliminary version appeared in Proceedings of the 41st Annual Symposium on Foundations of Computer Science (Redondo Beach, CA, 2000)). URL: https://doi.org/10.1137/S0097539701389944.
  4. Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, and Iddo Tzameret. Semialgebraic proofs, IPS lower bounds, and the τ-conjecture: Can a natural number be negative? SIAM J. Comput., 53(3):648-700, 2024. URL: https://doi.org/10.1137/20M1374523.
  5. Robert Andrews and Michael A. Forbes. Ideals, determinants, and straightening: proving and using lower bounds for polynomial ideals. In Proceedings of the 54th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2022, pages 389-402, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3519935.3520025.
  6. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc. (3), 73(1):1-26, 1996. URL: https://doi.org/10.1112/plms/s3-73.1.1.
  7. Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present and future. Bulletin of the EATCS, 65:66-89, 1998. Google Scholar
  8. Amik Raj Behera, Nutan Limaye, Varun Ramanathan, and Srikanth Srinivasan. New bounds for the ideal proof system in positive characteristic. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025), Aarhus, Denmark, July 2025. To appear. Google Scholar
  9. CS Bhargav, Sagnik Dutta, and Nitin Saxena. Improved lower bound, and proof barrier, for constant depth algebraic circuits. ACM Transactions on Computation Theory, 16(4):1-22, 2024. URL: https://doi.org/10.1145/3689957.
  10. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. The Journal of Symbolic Logic, 62(3):708-728, 1997. URL: https://doi.org/10.2307/2275569.
  11. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM J. Comput., 29(6):1939-1967, 2000. URL: https://doi.org/10.1137/S0097539798353230.
  12. Samuel R Buss. Polynomial size proofs of the propositional pigeonhole principle. The Journal of Symbolic Logic, 52(4):916-927, 1987. URL: https://doi.org/10.2307/2273826.
  13. Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiří Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity, 6(3):256-298, 1996. URL: https://doi.org/10.1007/BF01294258.
  14. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996), pages 174-183, New York, 1996. ACM. URL: https://doi.org/10.1145/237814.237860.
  15. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  16. Tal Elbaz, Nashlen Govindasamy, Jiaqi Lu, and Iddo Tzameret. Lower bounds against the ideal proof system in finite fields. arXiv preprint arXiv:2506.17210, 2025. URL: https://doi.org/10.48550/arXiv.2506.17210.
  17. Michael A Forbes. Low-depth algebraic circuit lower bounds over any field. In Rahul Santhanam, editor, 39th Computational Complexity Conference (CCC 2024), volume 300 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:16, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.31.
  18. Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson. Proof complexity lower bounds from algebraic circuit complexity. Theory Comput., 17:1-88, 2021. URL: https://doi.org/10.4086/TOC.2021.V017A010.
  19. Harvey Friedman. On the consistency, completeness and correctness problems. Unpublished, 1979. Google Scholar
  20. Michal Garlik, Svyatoslav Gryaznov, Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. Meta-mathematics of algebraic circuit lower bounds. Manuscript, 2025. Google Scholar
  21. Michal Garlik, Svyatoslav Gryaznov, Hanlin Ren, and Iddo Tzameret. The weak rank principle: Lower bounds and applications. Manuscript, 2025. Google Scholar
  22. Andreas Goerdt. Cutting plane versus Frege proof systems. In Egon Börger, Hans Kleine Büning, Michael M. Richter, and Wolfgang Schönfeld, editors, Computer Science Logic, 4th Workshop, CSL '90, Heidelberg, Germany, October 1-5, 1990, Proceedings, volume 533 of Lecture Notes in Computer Science, pages 174-194. Springer, 1991. URL: https://doi.org/10.1007/3-540-54487-9_59.
  23. Nashlen Govindasamy, Tuomas Hakoniemi, and Iddo Tzameret. Simple hard instances for low-depth algebraic proofs. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 188-199. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00025.
  24. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6):37:1-37:59, 2018. URL: https://doi.org/10.1145/3230742.
  25. Armin Haken. The intractability of resolution. Theoret. Comput. Sci., 39(2-3):297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  26. Tuomas Hakoniemi, Nutan Limaye, and Iddo Tzameret. Functional lower bounds in algebraic proofs: Symmetry, lifting, and barriers. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, pages 1396-1404, New York, NY, USA, 2024. Association for Computing Machinery. Full version in ECCC https://eccc.weizmann.ac.il/report/2024/079/. URL: https://doi.org/10.1145/3618260.3649616.
  27. Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. The surprising power of constant depth algebraic proofs. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 591-603. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394754.
  28. Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. URL: https://doi.org/10.2307/2275541.
  29. Jan Krajíček. On the proof complexity of the Nisan-Wigderson generator based on a hard NP∩coNP function. J. Math. Log., 11(1):11-27, 2011. URL: https://doi.org/10.1142/S0219061311000979.
  30. Jan Krajíček. Proof complexity, volume 170. Cambridge University Press, 2019. Google Scholar
  31. Jan Krajíček, Pavel Pudlák, and Alan Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures & Algorithms, 7(1):15-39, 1995. URL: https://doi.org/10.1002/rsa.3240070103.
  32. Jan Krajíček. Diagonalization in proof complexity. Fundamenta Mathematicae, 182:181-192, 2004. Google Scholar
  33. Jan Krajíček. Dual weak pigeonhole principles, pseudo-surjective functions, and provability of circuit lower bounds. Journal of Symbolic Logic, 69(1):265-286, 2004. URL: https://doi.org/10.2178/JSL/1080938841.
  34. Nutan Limaye, Srikanth Srinivasan, and Sébastien Tavenas. Superpolynomial lower bounds against low-depth algebraic circuits. Journal of the ACM, 72(4):1-35, 2025. URL: https://doi.org/10.1145/3734215.
  35. Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. Ac⁰[p]-frege cannot efficiently prove that constant-depth algebraic circuit lower bounds are hard. arXiv preprint arXiv:2509.16824, 2025. URL: https://doi.org/10.48550/arXiv.2509.16824.
  36. Jan Pich and Rahul Santhanam. Why are proof complexity lower bounds hard? In 60th Annual IEEE Symposium on Foundations of Computer Science FOCS 2019, November 9-12, 2019, Baltimore, Maryland USA, 2019. Google Scholar
  37. Ján Pich and Rahul Santhanam. Learning algorithms versus automatability of frege systems. Journal of Mathematical Logic, 2024. URL: https://doi.org/10.1142/S0219061325500023.
  38. Toniann Pitassi. Algebraic propositional proof systems. In Neil Immerman and Phokion G. Kolaitis, editors, Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop 1996, Princeton, New Jersey, USA, January 14-17, 1996, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 215-244, Providence, RI, 1997. American Mathematical Society. URL: https://doi.org/10.1090/DIMACS/031/07.
  39. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. computational complexity, 3(2):97-140, 1993. URL: https://doi.org/10.1007/BF01200117.
  40. Pavel Pudlak. On the length of proofs of finitistic consistency statements in first order theories. Studies in Logic and the Foundations of Mathematics, 120:165-196, 1986. Google Scholar
  41. Pavel Pudlak. Improved bounds to the length of proofs of finite consistency statements. Contemporary Mathematics, 65:309-331, 1987. Google Scholar
  42. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, September 1997. URL: https://doi.org/10.2307/2275583.
  43. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115-138, 2004. URL: https://doi.org/10.1145/972639.972640.
  44. Ran Raz. Elusive functions and lower bounds for arithmetic circuits. Theory of Computing, 6(1):135-177, 2010. URL: https://doi.org/10.4086/toc.2010.v006a007.
  45. Alexander Razborov. Propositional proof complexity: Fifteen (or so) years after. Talk at "A Celebration of Mathematics and Computer Science. Celebrating Avi Wigderson’s 60th Birthday October 5 - 8, 2016". https://youtu.be/7LfW6VTW8zo?t=2722, 2016.
  46. Alexander Razborov. P, NP and proof complexity. Talk at "SAT and Foundations of Mathematics", Simons Institute. https://youtu.be/xx4mxcqAl5A?t=2333, 2021.
  47. Alexander A. Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mathematical notes of the Academy of Sciences of the USSR, 41(4):333-338, 1987. URL: https://doi.org/10.1007/BF01137685.
  48. Alexander A. Razborov. Bounded arithmetic and lower bounds in boolean complexity. In Clote, P., Remmel, J., eds. Feasible Mathematics II. Progress in Computer Science and Applied Logic, volume 13, pages 344-86. Birkhauser, 1995. Google Scholar
  49. Alexander A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izv. Ross. Akad. Nauk Ser. Mat., 59(1):201-224, 1995. Google Scholar
  50. Alexander A. Razborov. Lower bounds for propositional proofs and independence results in bounded arithmetic. In Friedhelm Meyer auf der Heide and Burkhard Monien, editors, Automata, Languages and Programming, 23rd International Colloquium, ICALP96, Paderborn, Germany, 8-12 July 1996, Proceedings, volume 1099 of Lecture Notes in Computer Science, pages 48-62. Springer, 1996. URL: https://doi.org/10.1007/3-540-61440-0_116.
  51. Alexander A. Razborov. Lower bounds for the polynomial calculus. Comput. Complexity, 7(4):291-324, 1998. URL: https://doi.org/10.1007/S000370050013.
  52. Alexander A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, 181:415-472, 2015. Google Scholar
  53. Alexander A. Razborov. Guest column: Proof complexity and beyond. SIGACT News, 47(2):66-86, 2016. URL: https://doi.org/10.1145/2951860.2951875.
  54. Rahul Santhanam and Iddo Tzameret. Iterated lower bound formulas: A diagonalization-based approach to proof complexity. SIAM Journal on Computing, pages 313-349, 2025. Preliminary version appeared in Proceedings of the 53rd Annual ACM Symposium on Theory of Computing (STOC 2021). Google Scholar
  55. Amir Shpilka and Amir Yehudayoff. Arithmetic circuits: A survey of recent results and open questions. Foundations and Trends in Theoretical Computer Science, 5(3-4):207-388, 2010. URL: https://doi.org/10.1561/0400000039.
  56. Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proceedings of the Annual ACM Symposium on the Theory of Computing 1987, pages 77-82, 1987. URL: https://doi.org/10.1145/28395.28404.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact