Empirical Circuit Complexity

A research program to empirically prove the exact circuit complexity of concrete Boolean functions $\lbrace 0,1 \rbrace^n \to \lbrace 0,1 \rbrace$ for small $n$, with all results formally verified in Lean 4.

See paper/main.pdf for a detailed writeup.

Circuit model

A circuit is a DAG of fan-in 2 AND gates, where each wire (gate input or circuit output) carries an optional negation bit that flips the signal at zero cost. NOT is not a gate — it is simply an annotation on a wire. Circuit size is the number of AND gates.

This is equivalent to counting $\lbrace \text{AND}, \text{OR} \rbrace$ gates, since $\text{OR}(a,b) = \lnot\text{AND}(\lnot a, \lnot b)$ by De Morgan at zero additional cost.

Constants cost one gate. There are no free constant wires. The cheapest constant is $\text{AND}(x, \lnot x) = \mathsf{false}$ (one gate), optionally negated for $\mathsf{true}$.

Trust architecture

For each input size $n$, three kinds of files are produced:

1. Size<n>/Defs<m>.lean — Generated by a trusted Python program. Boolean functions encoded as (Fin n → Bool) → Bool.
2. Size<n>/Proofs<m>.lean — Written by AI. Upper bounds (witness circuits) and lower bounds (ruling out smaller circuits). The only files AI touches.
3. Size<n>/Statements<m>.lean — Generated by the same trusted program. Imports Defs and Proofs, states the complexity theorems.

We trust only the generator (which we review) and Lean's type checker. The AI is untrusted — incorrect proofs are rejected at type-checking time.

All proofs must be explicit. No native_decide or other opaque decision procedures.

Symmetry group

Three operations on circuits preserve size and are therefore free:

1. Input permutation ($S_n$): relabel input wires. Circuits.CircuitComplexity_perm
2. Input negation ($\mathbb{Z}_2^n$): flip negation bits on input wires. Circuits.CircuitComplexity_negInput
3. Output negation ($\mathbb{Z}_2$): flip the output negation bit. Circuits.CircuitComplexity_neg

These generate the NPN equivalence group

$$G = (S_n \ltimes \mathbb{Z}_2^n) \times \mathbb{Z}_2$$

of order $2^{n+1} \cdot n!$. The generator groups functions into equivalence classes under this group. Only one representative per class needs a proof.

$n$	Functions	$|G|$	Representatives	Reduction
1	$4$	$4$	$2$	$2\times$
2	$16$	$16$	$4$	$4\times$
3	$256$	$96$	$14$	$18\times$
4	$65{,}536$	$768$	$222$	$295\times$
5	$\sim 4.3 \times 10^9$	$7{,}680$	$616{,}126$	$6{,}971\times$

Truth table encoding

Function f_idx has truth table encoded by idx: bit $j$ of idx gives $f(\text{input}j)$, where $\text{input}j$ interprets $(x_0, \ldots, x{n-1})$ in little-endian binary as $x_0 \cdot 2^0 + x_1 \cdot 2^1 + \cdots + x{n-1} \cdot 2^{n-1}$.

For example, with $n = 2$, function index 6 (binary 0110) maps inputs $(0,0) \to 0$, $(1,0) \to 1$, $(0,1) \to 1$, $(1,1) \to 0$ — this is XOR.

Proof contract

Each Size<n>/Proofs<m>.lean file must export, for every representative function index idx in its batch:

• f_{idx}_size : Nat — the circuit complexity $k$
• f_{idx}_upper : HasCircuitOfSize f_{idx} k — a witness circuit
• f_{idx}_lower : ∀ j, j < k → ¬HasCircuitOfSize f_{idx} j — optimality

The Statements file combines these into a CircuitComplexity theorem.

Generator

The trusted generator lives at gen/generate.py:

python3 gen/generate.py 1 2 3              # generate for n = 1, 2, 3
python3 gen/generate.py --batch-size 8 3   # custom batch size

The default batch size is 16 functions per file.

Dependencies

Lean 4 (v4.28.0) with no external dependencies — no Mathlib or other libraries. This keeps the trusted base minimal.

Patterns

The patterns/ directory documents proof techniques and observations as they emerge:

• patterns/upper-bounds.md — witness circuit construction
• patterns/lower-bounds.md — lower bound proof structure
• patterns/observations.md — results tables and structural observations

Target

The initial target is $n = 1$ through $n = 4$, covering $4 + 16 + 256 + 65{,}536 = 65{,}812$ functions ($2 + 4 + 14 + 222 = 242$ representative proofs needed).

The goal is to gain knowledge on proving circuit lower bounds for concrete circuits, in the hope that the techniques and insights transfer to general purpose circuit lower bounds.