Why SAT solvers fail on multiplication
First exponential resolution lower bound for multiplier associativity; ‘main ideas and the core proof … are due to GPT-5.6-Sol’ (Liew)
Awaiting review
The takeaway
SAT solvers are known to choke on multiplication, but nobody had proved that short proofs do not exist. Vincent Liew’s preprint proves an exponential lower bound for resolution proofs that n-bit multiplication is associative, resolving an open problem he had posed with Paul Beame. He credits the main ideas and the core proof to GPT-5.6 Sol; a Lean 4 formalization was generated by Claude Fable 5.1.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 13 October 2026
Your AI and this story
- GPT-6 Astra159 days after its cutoff
- Claude Opus 5.598 days after its cutoff
- Gemini 3.8 Flash189 days after its cutoff
- Grok 4.7128 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 98 days before it.
Key facts
- Paper: ‘Associativity of Multiplication Is Hard for Resolution’, arXiv 2610.08988 [cs.CC], 6 Oct 2026, 33 pages; Vincent Liew
- Result: resolution proofs of associativity of n-bit multiplication ‘require size 2^Ω((n/log n)^(1/4))’; the bound ‘holds for a broad class of multiplier encodings based on partial product summation, including the standard array and Wallace-tree multipliers used to bit-blast multiplication in SMT solvers’
- Motivation (abstract): ‘SAT solvers are empirically known to perform poorly when reasoning about multiplication. Yet for over a decade we have lacked a theoretical explanation for this phenomenon. CDCL SAT solvers implicitly search for resolution proofs, and no lower bound on proof size has ruled out the existence of short proofs that solvers simply fail to find.’
- Method: a reduction from a perfect-matching principle on bounded-degree bipartite expander graphs, which Itsykson, Slabodkin and Sokolov proved hard for resolution, to multiplier associativity
- Extension: combined with Håstad’s recent lower bound for the perfect-matching principle of the odd grid, the same reduction ‘yields an exponential lower bound for multiplier associativity in the stronger bounded-depth Frege proof systems’
- AI Methodology: ‘The main ideas and the core proof of the associativity lower bound are due to GPT-5.6-Sol. This materially affected Sections 5, 7, 8, and 9, and Appendix A. During the verification process, the author reformulated and rewrote the definitions, lemma statements, and proofs with the assistance of Claude Fable 5, and added attributions along the way.’
- Also: ‘The Lean formalization (Appendix B) was generated by Claude Fable 5.1.’ and ‘The author verified the correctness and originality of all content, including references, and takes full responsibility for the paper’s content.’
- Caveat on the Lean proof (paper): the formalization includes its own definitions of the circuits; ‘While we have inspected these definitions ourselves, we caution that they are a potential source of error.’
Show 1 more
- Lean 4 code: github.com/dysfunctor/associativity
What happened
Modern SAT solvers (CDCL solvers) can be seen as searching for proofs in a simple system called resolution. They are fast on many hardware-verification tasks but notoriously slow on anything involving multiplication, such as checking that two multiplier circuits compute the same function or that (xy)z = x(yz) for n-bit numbers. It was not known whether this is a weakness of the solvers’ search or a real limit, meaning that short resolution proofs do not exist at all.
Liew’s preprint proves the second for associativity: any resolution proof has size exponential in roughly the fourth root of n. The proof embeds a perfect-matching principle on expander graphs, already known to be hard for resolution, into the associativity statement. With a recent result of Håstad the argument extends to bounded-depth Frege systems, which are stronger than resolution.
The paper says that the main ideas and the core proof come from GPT-5.6 Sol, that the author checked and rewrote them with Claude Fable 5, and that Claude Fable 5.1 produced a Lean 4 formalization of the main theorems.
Why it matters
It gives the first theoretical explanation for an effect that practitioners in verification have worked around for more than a decade, on a question posed by specialists in proof complexity. It is also a clear instance of the 2026 pattern in theoretical computer science: the model supplies the reduction, a second model formalizes it, and the human author’s work is verification and exposition.
What is disputed or not yet verified
| Verification | Lean 4 formalization of the main theorems generated by Claude Fable 5.1 (circuit definitions inspected by the author, flagged as a possible source of error); unrefereed preprint |
|---|
The Lean development was not run for this entry. The paper gives no affiliation for the author and none is stated here. No expert reaction or Hacker News discussion was found on 13 Oct 2026.
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
- arXiv 2610.08988: Associativity of Multiplication Is Hard for Resolutionarxiv.org, paper
- Lean 4 formalization (dysfunctor/associativity)github.com, code
Changes
- Filed from the arXiv PDF