Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication
Multiplying two four-term binary polynomials needs exactly nine AND gates even when nonlinear intermediate wires may be reused, with the whole result formalized in Lean 4.
- Lab
- Independent
- Model
- GPT-5.6 Sol; Claude Opus 5
- Field
- Computer science
- Date
- 2026-08-31
- Human collaborators
- Gregory Morse
- Problem posed
- 2014 · open 12 yrs
Sources
Original work
Independent commentary
What was found
Classical lower bounds show that multiplying two degree-three polynomials over the field with two elements needs nine scalar products in bilinear or quadratic models, but they leave open the unrestricted Boolean case, where an XOR-AND circuit may reuse nonlinear intermediate wires and equality is taken modulo the idempotence relations, so a multiplication can lower algebraic degree. The paper proves that the map producing the seven coefficients of the product of two four-term binary polynomials has unrestricted XOR-AND multiplicative complexity exactly nine. This resolves, for a natural vector-valued quadratic function, the Boyar-Find question of whether a quadratic-circuit lower bound survives unrestricted nonlinear reuse. The proof is structural rather than exhaustive, and the same argument gives multiplicative complexity six for three-term multiplication.
Novelty check
The open question is attributed to Boyar and Find and dated 2014, and the paper is explicit about what the classical bounds do and do not settle: they cover bilinear and quadratic models, not unrestricted Boolean circuits with nonlinear reuse. That distinction is the entire content of the contribution and is stated before the result. No prior unrestricted lower bound for this function appears.
Caveats and known objections
A preprint days old at entry, unrefereed, with no independent human check on record, and vibemathed records the resolution as partial since this settles one function rather than the general question. The formal grade is well supported for a self-published result: the Lean 4 formalization covers the Boolean-ANF semantics, the unrestricted circuit model, the seven- and eight-gate exclusions and the explicit nine-gate upper bound, uses no project-specific axiom and no native decision procedure, pins Lean v4.32.1 and a locked mathlib revision, and its continuous integration performs the build, an axiom audit and a declaration replay with a weekly fresh source replay. What is missing is third-party auditing that the formalized statements say what the paper says. Autonomy is graded ai-assisted, matching the disclosed roles, with GPT-5.6 Sol at an extra-high setting and Claude Opus 5 acting as a referee.
Also recorded at
vibemathedunrestricted-multiplicative-complexity-mul4
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-assisted.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-assisted for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-31-boolean-multiplicative-complexity-mul4BibTeX
@misc{whataifound-independent-2026-mul4,
title = {Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-assisted.},
url = {https://whataifound.org/finding/2026-08-31-boolean-multiplicative-complexity-mul4}
}