Unrestricted Boolean multiplicative complexity of four-term polynomial multiplication

Does multiplying two four-term binary polynomials require nine AND gates even when an XOR–AND circuit may reuse nonlinear intermediate values?

Aug 31, 2026

Exact nine-gate lower and upper bound

Model / AI: GPT-5.6 Sol, Claude Opus 5

machine-checkedself-reported

Gregory Morse reports AI assistance in developing a structural proof that unrestricted multiplicative complexity is exactly nine, with Claude used for adversarial review. A Lean 4 development covers the circuit semantics, lower-bound exclusions and explicit upper bound.

Source read 2026-09-08. Read the abstract and formalization scope in arXiv v1. The linked Lean project was not rebuilt or semantically audited.

Paper — Paper
Lean — Lean artifact