Document Open Access Logo

Meta-Mathematics of Algebraic Complexity

Authors Michal Garlík , Svyatolav Gryaznov , Jiaqi Lu , Rahul Santhanam , Iddo Tzameret

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.49.pdf
  • Filesize: 0.95 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Algebraic complexity theory
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Proof theory
  • Theory of computation → Proof complexity
  • Theory of computation → Circuit complexity
Keywords
  • Complexity lower bounds
  • Bounded arithmetic
  • Feasible constructive mathematics
  • Algebraic complexity
  • Proof complexity
  • Meta-complexity
  • Algebraic circuit lower bounds
  • Polynomial Calculus Resolution
  • Barriers

Metrics

Abstract

We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as polynomial calculus resolution (PCR), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to NC², such as VNC² and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below VNC² into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Specifically, we show the following.
- NC²-reasoning and rank method. Algebraic circuit lower bounds are often proved via the "rank method", with recent prominent applications including the constant-depth lower bounds of Limaye, Srinivasan and Tavenas [Limaye et al., 2025] and Forbes [Forbes, 2024]. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC², which captures reasoning with NC² concepts. This complements the work of Tzameret and Cook [Tzameret and Cook, 2021], who formalized structural upper bounds in this theory, and provides a unified framework for studying barriers to current algebraic complexity methods, complementing barriers studied by Efremenko, Garg, Makam, Oliveira, and Wigderson [Klim Efremenko et al., 2018; Ankit Garg et al., 2019].
- Sparsity algebraic reasoning. We show that Polynomial Calculus Resolution (PCR) cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, PCR cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials.
- Constant-depth algebraic reasoning. We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System (IPS) then constant-depth IPS cannot efficiently prove constant-depth algebraic circuit lower bounds.

Cite As Get BibTex

Michal Garlík, Svyatolav Gryaznov, Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. Meta-Mathematics of Algebraic Complexity. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 49:1-49:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.49

Author Details

Michal Garlík
  • Imperial College London, UK
Svyatolav Gryaznov
  • Imperial College London, UK
Jiaqi Lu
  • Imperial College London, UK
Rahul Santhanam
  • Oxford University, UK
Iddo Tzameret
  • Imperial College London, UK

Funding

  • Garlík, Michal: 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).
  • Gryaznov, Svyatolav: 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).
  • 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). It was also supported by the Engineering and Physical Sciences Research Council (EPSRC) under grant EP/Z534158/1.
  • Santhanam, Rahul: This project was partly funded by the EPSRC grant EP/Z534158/1.
  • 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.

Acknowledgements

We are indebted to the anonymous reviewers of this paper for many important comments.

References

  1. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM J. Comput., 31(4):1184-1211 (electronic), 2002. Google Scholar
  2. Per Austrin and Kilian Risse. Sum-of-squares lower bounds for the minimum circuit size problem. In 38th Computational Complexity Conference, CCC'23, pages 31:1-31:21, 2023. URL: https://doi.org/10.4230/LIPIcs.CCC.2023.31.
  3. Theodore P. Baker, John Gill, and Robert Solovay. Relativizations of the P =? NP question. SIAM J. Comput., 4(4):431-442, 1975. URL: https://doi.org/10.1137/0204037.
  4. 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.
  5. Peter Bürgisser, Michael Clausen, and M. Amin Shokrollahi. Algebraic complexity theory, volume 315 of Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, Berlin, 1997. Google Scholar
  6. Prerona Chatterjee, Mrinal Kumar, C. Ramya, Ramprasad Saptharishi, and Anamay Tengse. On the existence of algebraically natural proofs. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS '20, pages 870-880. IEEE, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00085.
  7. Lijie Chen, Jiatu Li, and Igor Oliveira. Reverse mathematics of complexity lower bounds. SIAM Journal on Computing, pages FOCS24-316, 2026. Google Scholar
  8. Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. ASL Perspectives in Logic. Cambridge University Press, 2010. Google Scholar
  9. Klim Efremenko, Ankit Garg, Rafael Mendes de Oliveira, and Avi Wigderson. Barriers for rank methods in arithmetic complexity. In 9th Innovations in Theoretical Computer Science Conference, ITCS'18, pages 1:1-1:19, 2018. URL: https://doi.org/10.4230/LIPIcs.ITCS.2018.1.
  10. Michael A. Forbes. Low-Depth Algebraic Circuit Lower Bounds over Any Field. In 39th Computational Complexity Conference (CCC 2024), volume 300 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.31.
  11. 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.
  12. Michael A. Forbes, Amir Shpilka, and Ben Lee Volk. Succinct hitting sets and barriers to proving lower bounds for algebraic circuits. Theory of Computing, 14(1):1-45, 2018. URL: https://doi.org/10.4086/toc.2018.v014a018.
  13. Ankit Garg, Visu Makam, Rafael Mendes de Oliveira, and Avi Wigderson. More barriers for rank methods, via a "numeric to symbolic" transfer. In 60th IEEE Annual Symposium on Foundations of Computer Science, FOCS '19, pages 824-844, 2019. URL: https://doi.org/10.1109/FOCS.2019.00054.
  14. Michal Garlík, Svyatoslav Gryaznov, Ren Hanlin, and Iddo Tzameret. The weak rank principle: Lower bounds and applications. In Proceedings of the 58th Annual ACM Symposium on the Theory of Computing (STOC), 2026. Google Scholar
  15. Joshua A. Grochow, Mrinal Kumar, Michael E. Saks, and Shubhangi Saraf. Towards an algebraic natural proofs barrier via polynomial identity testing. CoRR, abs/1701.01717, 2017. URL: https://arxiv.org/abs/1701.01717.
  16. 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.
  17. Joel David Hamkins and Emil Jeřabek. Can the induction axiom in the peano arithmetic be replaced by the irrationality of √2? MathOverflow (2018). URL: https://mathoverflow.net/q/306860.
  18. Pavel Hrubes and Iddo Tzameret. Short proofs for the determinant identities. SIAM J. Comput., 44(2):340-383, 2015. URL: https://doi.org/10.1137/130917788.
  19. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  20. Emil Jeřábek. Elementary analytic functions in VTC⁰. Annals of Pure and Applied Logic, 174(6):103269, 2023. Google Scholar
  21. Eitetsu Ken and Satoru Kuroda. On matrix rank function over bounded arithmetics. arXiv preprint arXiv:2310.05982, 2023. URL: https://doi.org/10.48550/arXiv.2310.05982.
  22. Jan Krajíček. Bounded arithmetic, propositional logic, and complexity theory, volume 60 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511529948.
  23. 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.
  24. 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.
  25. Mrinal Kumar, C. Ramya, Ramprasad Saptharishi, and Anamay Tengse. If VNP is hard, then so are equations for it. In 39th International Symposium on Theoretical Aspects of Computer Science, STACS'22, pages 44:1-44:13, 2022. URL: https://doi.org/10.4230/LIPIcs.STACS.2022.44.
  26. Jiatu Li and Igor C Oliveira. Unprovability of strong complexity lower bounds in bounded arithmetic. In Proceedings of the 55th Annual ACM Symposium on Theory of Computing, pages 1051-1057, 2023. URL: https://doi.org/10.1145/3564246.3585144.
  27. 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.
  28. 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 '26, 2026. arXiv preprint arXiv:2509.16824. URL: https://doi.org/10.48550/arXiv.2509.16824.
  29. Henryk Minc. Evaluation of permanents. Proceedings of the Edinburgh Mathematical Society, 22(1):27-32, 1979. Google Scholar
  30. Moritz Müller and Ján Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic, 171(2):102735, 2020. URL: https://doi.org/10.1016/j.apal.2019.102735.
  31. Ketan Mulmuley. A fast parallel algorithm to compute the rank of a matrix over an arbitrary field. In Proceedings of the eighteenth annual ACM symposium on Theory of computing, pages 338-339, 1986. URL: https://doi.org/10.1145/12130.12164.
  32. Igor C Oliveira. Sigact news complexity theory column 124 meta-mathematics of computational complexity theory. ACM SIGACT News, 56(1):41-68, 2025. URL: https://doi.org/10.1145/3726856.3726862.
  33. 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.
  34. 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.
  35. Alexander Razborov. P, NP and proof complexity. Talk at "SAT and Foundations of Mathematics", Simons Institute. https://youtu.be/xx4mxcqAl5A?t=2333, 2021.
  36. 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
  37. 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
  38. Alexander A. Razborov. Lower bounds for propositional proofs and independence results in bounded arithmetic. In Automata, Languages and Programming, 23rd International Colloquium, ICALP '96, pages 48-62. Springer, 1996. URL: https://doi.org/10.1007/3-540-61440-0_116.
  39. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, 1998. URL: https://doi.org/10.1007/s000370050013.
  40. Alexander A. Razborov. Resolution lower bounds for perfect matching principles. Journal of Computer and System Sciences, 2004. Google Scholar
  41. Alexander A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, 181:415-472, 2015. Google Scholar
  42. Alexander A. Razborov. Guest column: Proof complexity and beyond. SIGACT News, 47(2):66-86, 2016. URL: https://doi.org/10.1145/2951860.2951875.
  43. Alexander A. Razborov and Steven Rudich. Natural proofs. J. Comput. System Sci., 55(1, part 1):24-35, 1997. URL: https://doi.org/10.1006/JCSS.1997.1494.
  44. Rahul Santhanam and Iddo Tzameret. Iterated lower bound formulas: A diagonalization-based approach to proof complexity. SIAM Journal on Computing, 0(0):STOC21-313-STOC21-349, 0. URL: https://doi.org/10.1137/21M1447519.
  45. 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.
  46. 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.
  47. Iddo Tzameret and Stephen A Cook. Uniform, integral, and feasible proofs for the determinant identities. Journal of the ACM (J. ACM), 68(2):1-80, 2021. URL: https://doi.org/10.1145/3431922.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact