一句话：在 VNC2 中证明整数上行列式乘法性，给出统一的 O(log²n)-深度多项式规模 Circuit-Frege 证明及 NC2 代数电路算法。
本文研究行列式恒等式在整数上的短命题证明能否统一且高效。此前 Hrubeš 与 Tzameret 仅在 GF(2) 上给出了短证明。作者在对应 NC2 的有界算术理论 VNC2 中形式化了行列式函数的乘法性，并据此构造出整数上基本行列式恒等式的统一多项式规模、O(log² n) 深度 Circuit-Frege（等价 Extended Frege）证明。为完成证明，还给出 VNC2 中 Σ1B-可定义的统一 NC2 算法：齐次化代数电路、平衡代数电路（给定语法次数上界），以及把带除法门电路转换为仅含单个除法门的电路。这些算法也蕴含任意深度代数电路的 NC2 求值算法。
We give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubeš-Tzameret [9]. Specifically, we show that the multiplicativity of the determinant function over the integers is provable in the bounded arithmetic theory VNC2, which is a first-order theory corresponding to the complexity class NC2. This also establishes the existence of uniform polynomial-size and O(log2n)-depth Circuit-Frege (equivalently, Extended Frege) proofs over the integers, of the basic determinant identities (previous proofs hold only over GF(2)). In doing so, we give uniform NC2-algorithms for homogenizing algebraic circuits, balancing algebraic circuits (given as input an upper bound on the syntactic-degree of the circuit), and converting circuits with divisions into circuits with a single division gate-all (Σ1B-) definable in VNC2. This also implies an NC2-algorithm for evaluating algebraic circuits of any depth.