Papers With

← All papers
First page of Formalizing PARITY Circuit Lower Bounds in Lean

Formalizing PARITY Circuit Lower Bounds in Lean

Saint Wesonga

cs.CC Sep 21, 2026 · v1 cs.LO
formalization logic
Read PDF arXiv abstract Code
TL;DR
Formalizes Håstad's switching-lemma PARITY circuit lower bound for constant-depth formulas and DAG circuits in Lean 4 with Mathlib.
Abstract
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.
Problem

Håstad's lower bound shows that constant-depth circuits computing PARITY on n inputs require size exp(Omega_d(n^(1/(d-1)))), implying PARITY is not in nonuniform AC0. This classical complexity-theory result had not been machine-checked.

Approach

Boolean formulas and DAG circuits with unbounded-fan-in AND/OR and NOT gates are defined inductively in Lean, along with DNF/CNF, size, width, and PARITY-computation predicates. NOT-gate elimination via De Morgan pushing, restriction lemmas, and the switching lemma are formalized to prove the formula lower bound. The bound is transferred to DAG circuits by unfolding into equivalent formulas with controlled depth and size blowup from duplicated shared gates.

Results

For every fixed depth d>=2 and sufficiently large n, well-formed circuits computing PARITY are proven to require size exp(Omega_d(n^(1/(d-1)))), matching the classical upper bound and formally establishing PARITY not in nonuniform AC0. A polynomial-size logarithmic-depth formula family witnesses NC1 not a subset of AC0 for the formalized models. Checked with Lean 4.33.1 and Mathlib 4.33.1.