--- id: "2026-10-06-multiplier-associativity-hard-for-resolution-gpt-5-6-sol" url: "https://postcutoff.com/e/2026-10-06-multiplier-associativity-hard-for-resolution-gpt-5-6-sol/" as_of: "2026-10-13T07:38:00+02:00" date: "2026-10-06" date_precision: day category: science importance: 3 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 2 editor: Adam Bicz human_review: null version: null --- As of: 2026-10-13 07:38 CEST. Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz. Canonical page: https://postcutoff.com/e/2026-10-06-multiplier-associativity-hard-for-resolution-gpt-5-6-sol/ # Why SAT solvers fail on multiplication Full title: 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) On 6 Oct 2026 Vincent Liew posted arXiv 2610.08988, "Associativity of Multiplication Is Hard for Resolution". It shows that general resolution proofs of the associativity of n-bit multiplication need size 2^Ω((n/log n)^(1/4)), for a broad class of multiplier encodings that includes the array and Wallace-tree multipliers used by SMT solvers. The abstract calls it the first lower bound of this kind and says it "resolves an open problem of Beame and Liew". The paper's "AI Methodology" section states: "The main ideas and the core proof of the associativity lower bound are due to GPT-5.6-Sol." Claude Fable 5 helped rewrite the proofs and Claude Fable 5.1 generated a Lean 4 formalization of the main theorems. Unrefereed preprint. ## 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.' - 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. ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff - Gemini 3.8 Flash (training cutoff March 2026): 189 days after its cutoff - Grok 4.7 (training cutoff May 2026): 128 days after its cutoff ## Sources 1. [arXiv 2610.08988: Associativity of Multiplication Is Hard for Resolution](https://arxiv.org/abs/2610.08988) (arxiv.org, paper) 2. [Lean 4 formalization (dysfunctor/associativity)](https://github.com/dysfunctor/associativity) (github.com, code) ## Changes - 2026-10-13 (filed): Created from the arXiv PDF ## Related - 2026-10-08: [Laderman's 23 multiplications are optimal for 3×3 matrices over F_2 and over the integers](https://postcutoff.com/e/2026-10-08-rank-3x3-matrix-multiplication-f2-is-23-lean-tomar/index.md) - 2026-10-06: [Preprint claims a 4.268 upper bound for the random 3-SAT threshold, down from 4.4898, with a Lean 4 proof; 'large language models drove the research'](https://postcutoff.com/e/2026-10-06-random-3-sat-threshold-upper-bound-4-268-llm/index.md) - 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md)