Search Results

Documents authored by Lu, Jiaqi

Document
DOI: 10.4230/LIPIcs.LICS.2026.49
Meta-Mathematics of Algebraic Complexity

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

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{garlik_et_al:LIPIcs.LICS.2026.49,
  author =	{Garl{\'\i}k, Michal and Gryaznov, Svyatolav and Lu, Jiaqi and Santhanam, Rahul and Tzameret, Iddo},
  title =	{{Meta-Mathematics of Algebraic Complexity}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{49:1--49:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.49},
  URN =		{urn:nbn:de:0030-drops-268360},
  doi =		{10.4230/LIPIcs.LICS.2026.49},
  annote =	{Keywords: Complexity lower bounds, Bounded arithmetic, Feasible constructive mathematics, Algebraic complexity, Proof complexity, Meta-complexity, Algebraic circuit lower bounds, Polynomial Calculus Resolution, Barriers}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2026.99
AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard

Authors: Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.ITCS.2026.99,
  author =	{Lu, Jiaqi and Santhanam, Rahul and Tzameret, Iddo},
  title =	{{AC⁰\lbrackp\rbrack-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{99:1--99:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2026.99},
  URN =		{urn:nbn:de:0030-drops-253865},
  doi =		{10.4230/LIPIcs.ITCS.2026.99},
  annote =	{Keywords: Complexity, Lower bounds, Proof complexity, AC⁰\lbrackp\rbrack-Frege, Diagonalisation, Algebraic complexity}
}
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