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.
Independent checks
vibemathed.com rebuild: Rebuilt release n4-arxiv-v2 from source on the pinned toolchain, ran the axiom audit and replayed the whole environment with leanchecker: all six headline theorems use only the three standard axioms, with no sorry, project axiom, native_decide or bv_decide. The statements were not audited against the Boyar-Find question. · link ↗
Machine-checked elsewhere
PalomarPALOMAR-2026-09-21-000005
GregoryMorse/unrestricted-boolean-mul at 56837b8ed4ff · checked 2026-09-21
ProvedUnrestrictedBooleanMul.mc_mul_zeroUnrestrictedBooleanMul.mc_mul_oneUnrestrictedBooleanMul.mc_mul_twoUnrestrictedBooleanMul.mc_mul_threeUnrestrictedBooleanMul.N4.no_eight_gate_circuitUnrestrictedBooleanMul.N4.mc_mul_four
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Registered by the author. Palomar's record states that the open unrestricted and bilinear lower bounds for five and six terms are not claims of this submission.
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.
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
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.
History of this entry
- CorrectedRecorded the author's Palomar registration, PALOMAR-2026-09-21-000005, alongside the vibemathed record. source ↗
- CheckedRecorded vibemathed's rebuild of the Lean development from source, which confirms the axiom audit. It checks the build, not whether the statements match the paper, so no grade moved. source ↗
- 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}
}