Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication
Let Mul4: F_2^8 -> F_2^7 output the seven coefficients of the product of two four-term binary polynomials. The manuscript proves that its unrestricted XOR--AND multiplicative complexity is exactly 9. The upper bound is a nine-AND Karatsuba--Ofman construction. The lower bound rules out every unrestricted eight-AND circuit, including circuits that reuse nonlinear intermediate wires and exploit Boolean idempotence. Thus, for this natural vector-valued quadratic function, allowing nonlinear feedback does not improve on the optimal quadratic circuit.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Circuit complexity
- Posed by
- Joan Boyar and Magnus Gausdal Find
- Year posed
- 2014
- Years open
- 12y
- Solved
- 2026-08
- Model
- OpenAI GPT-5.6 Sol (extra-high); Anthropic Opus 5 (high, referee)
- Vendor
- OpenAI; Anthropic
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 12 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The exact Mul4 instance is resolved: its unrestricted XOR--AND multiplicative complexity is 9. The restricted bilinear/quadratic value 9 was classical; the new theorem proves that arbitrary nonlinear Boolean reuse cannot lower it. This is a natural positive special case of the Boyar--Find question, not a solution of the general (n,m) problem. The lower bound is a conceptual structural argument. A complete Lean 4 formalization checks the unrestricted circuit semantics and the exact equality, while the development-time Python/C++ programs remain independent regression checks rather than logical premises. The corresponding unrestricted questions for five or more terms remain open. Independent statement-fidelity review remains pending.
What the AI did
OpenAI GPT-5.6 Sol in extra-high thinking mode was used for research, proof exploration and development, computational checking, Lean 4 formalization and formal-proof engineering, literature and citation verification, manuscript drafting and revision, and release and submission preparation. Anthropic Opus 5 in high thinking mode was used as a critical referee, not as the discovery model. The public disclosure does not attribute a named essential lemma or the central informal proof solely to a model, so the conservative AI-assisted tier is retained rather than AI co-developed or AI-discovered. Gregory Morse directed and reviewed the mathematical claims, informal and formal proofs, computations, citations, code, and manuscript text and assumes full responsibility.
Verification
Lean-checked, statement unaudited. The complete unrestricted theorem is formalized in Lean 4.32.1 with a locked mathlib revision. The exported declaration is `UnrestrictedBooleanMul.N4.mc_mul_four : MC(Mul 4) = 9`; the project also exports the exact values for n=0,1,2,3. The source contains no `sorry`, `admit`, project-specific axiom, `native_decide`, or `bv_decide`; its axiom audit reports only `propext`, `Classical.choice`, and `Quot.sound`. GitHub Actions run 33354439833 passed `lake build`, `AxiomAudit.lean`, and `leanchecker` on commit 1533276ba8e9c9974a8eaf3a7f0d26d06db4be8a in 24m22s (the build itself took 20m33s). The final submission will point to immutable release `n4-arxiv-v2` and its exact commit. No independent audit of the informal-to-formal statement correspondence is yet claimed, so this is not labeled Lean-verified. The Python/C++ regression outputs are not trusted premises of the Lean theorem.
Sources
- PaperarXiv
- Lean proofComplete Lean proof and immutable verification release
- Lean statementHeadline theorem MC(Mul 4) = 9
- Problem recordBoyar--Find finite-field question
Submitted by SwiftFerret455 on