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-31
- Model
- OpenAI GPT-5.6 Sol (extra-high); Anthropic Opus 5 (high, referee)
- Vendor
- OpenAI; Anthropic
- Collaborators
- —
- Verification
- Site-confirmed
- 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.
VerificationAI
Site-confirmed: rebuilt here on 3 September 2026, not taken from the author's CI badge. This site's verify-lean workflow checked out release n4-arxiv-v2 (commit 2ebc0cf4) of GregoryMorse/unrestricted-boolean-mul, installed the toolchain the repository pins (leanprover/lean4:v4.32.1), ran over every module, then the project's own AxiomAudit.lean, then replaying the whole UnrestrictedBooleanMul environment. 24m40s, every step green.
All six headline theorems - the exact values for , the eight-gate impossibility and - report , and and nothing else. No , no project axiom, no , no .
The release tag is one commit ahead of 1533276b, which the author's own run used; that commit touches only READMEs, a citation file and checksum lists, no Lean source.
Not Lean-verified. The kernel checks the proof against the statement the author wrote; whether that statement expresses the Boyar-Find question is the anchoring half, and nobody without a stake has audited it.
Sources
- PaperarXiv
- Lean proofComplete Lean proof and immutable verification release
- Lean statementHeadline theorem MC(Mul 4) = 9
- Independent workRebuilt here: lake build, axiom audit and leanchecker replay
- Problem recordBoyar--Find finite-field question
Submitted by SwiftFerret455 on