在 Lean 中形式化 PARITY 电路下界
Formalizing PARITY Circuit Lower Bounds in Lean
- University of Wyoming（怀俄明大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
在 Lean 中形式化 Håstad 的 PARITY 下界，证明深度受限电路需指数规模，并构造 NC1 非 AC0 子集的见证。
AI中文摘要：
我们使用切换引理在 Lean 中形式化了 Håstad 的 PARITY 下界。对于每个固定的 d >= 2，计算 n 个输入上的 PARITY 的计算深度至多为 d 的公式和 DAG 电路，对于所有足够大的 n，需要规模 exp(Omega_d(n^(1/(d-1))))。这与经典上界在指数中的常数内匹配，并意味着 PARITY 不在非均匀 AC0 中。我们还构造了一个多项式大小、对数深度的有界扇入公式族用于 PARITY，为形式化模型提供了 NC1 不是 AC0 的子集的见证。Lean 源代码可在该 https URL 获取，并使用 Lean 4.33.1 和 mathlib 4.33.1 进行了检查。
英文摘要：
We formalize Hastad's PARITY lower bound in Lean using the switching lemma. For every fixed d >= 2, formulas and DAG circuits of computation depth at most d computing PARITY on n inputs require size exp(Omega_d(n^(1/(d-1)))) for all sufficiently large n. This matches the classical upper bound up to constants in the exponent and implies that PARITY is not in nonuniform AC0. We also construct a polynomial-size, logarithmic-depth bounded-fan-in formula family for PARITY, providing a witness to NC1 is not a subset of AC0 for the formalized models. The Lean source code is available at https://github.com/formalcs/circuit-complexity and is checked with Lean 4.33.1 and mathlib 4.33.1.
