# Formalizing PARITY Circuit Lower Bounds in Lean

Preprint · Saint Wesonga

- Archive id: arxiv:2609.24188
- Published: 2026-09-21
- arXiv: https://arxiv.org/abs/2609.24188
- Source URL: https://arxiv.org/abs/2609.24188
- PDF: https://arxiv.org/pdf/2609.24188
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.