Is block sensitivity at most quadratic in spectral sensitivity? (Aaronson, Ben-David, Kothari, Rao and Tal)

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , the spectral sensitivity $\lambda(f)$ is the largest eigenvalue of the adjacency matrix of its sensitivity graph (the hypercube edges across which $f$ changes value), and the block sensitivity $\mathrm{bs}(f)$ is the largest number of disjoint blocks of bits each of whose flip changes $f$ at some input. Huang's proof gives $\deg(f)\le\lambda(f)^2$ , and with Nisan-Szegedy $\mathrm{bs}(f)=O(\lambda(f)^4)$ . Aaronson, Ben-David, Kothari, Rao and Tal asked: is $\mathrm{bs}(f)=O(\lambda(f)^2)$ ?

Result: Disproved(see note)
Status: Candidate (review pending)
AI contribution: AI co-developed
Method: Construction
Field: Boolean function complexity; sensitivity
Posed by: Scott Aaronson, Shalev Ben-David, Robin Kothari, Shravas Rao and Avishay Tal, Degree vs. approximate degree and quantum implications of Huang's sensitivity theorem (STOC 2021), Section 7
Year posed: 2020
Years open: 6y
Solved: 2026-08-01
Model: GPT-5.6-Sol (ideas); Claude Opus 5 with Harmonic's Aristotle (Lean)
Vendor: OpenAI; Anthropic; Harmonic
Collaborators: Alexander Meiburg
Verification: Lean-checked, statement unaudited
Publication: Preprint
Significance: 22 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 6.1: a total Boolean function on 2,017,584 variables with $\mathrm{bs}(f)\ge14011$ and $\lambda(f)\le89.0162$ , so $\mathrm{bs}(f)\ge\lambda(f)^{2.127}$ ; composition gives a family with $\lambda\to\infty$ and $\mathrm{bs}=\Omega(\lambda^{2.127})$ , so no quadratic bound holds. The function is a union of subcubes indexed by a doubly regular tournament with gates fixed by the Lovász local lemma. An exponent near 2.20 on 1,255 variables is numerical evidence only. The true exponent, between 2.127 and 4, stays open. Since $\lambda(f)\le s(f)$ , OpenAI's later disproof of $\mathrm{bs}=O(s^2)$ (25 September 2026), which adapts this gated-tournament construction, implies this result.

What the AI did

The paper's Note on AI Usage: "Several key ideas of the proof, in particular that 'gated tournaments' would be a good candidate for large bs relative to lambda, were suggested by GPT-5.6-Sol. The initial proposed construction was on 269 variables. All text in this paper was produced without generative AI tooling, and the author is responsible for the exposition, minimizing and optimizing size and parameters, and verifying the faithfulness of the Lean formalization." The paper says the formalization was carried out using Aristotle; the repository's formalization.yaml records a Claude Code session on Claude Opus 5 with about a dozen goal-level human turns, plus Harmonic's prover for leaf lemmas.

Verification

Checked here on 7 October 2026: Theorem 6.1 and Corollary 6.2 of arXiv:2608.00851 were read against the question as printed in Section 7 of Aaronson, Ben-David, Kothari, Rao and Tal. In Timeroot/BS_Lam, BSLambda/Main.lean was read: exists_bs_gt_lam_rpow states a total Boolean function on ZMod 14011 x Fin 144 inputs with $\lambda(f)^{2.12}<\mathrm{bs}(f)$ (the comparator challenge printed in the paper's Appendix B), and exists_ratio_blowup states $(14011/U)^m\lambda(F_m)^2\le\mathrm{bs}(F_m)$ for the $m$ -fold self-compositions, with $14011/U>1$ , which is the unbounded-ratio disproof. The definitions of bs, the sensitivity-graph adjacency matrix and its top eigenvalue match the paper. The repository reports no sorry and only propext, Classical.choice and Quot.sound, and proves the multiplicativity of $\lambda$ under composition rather than importing it. Not rebuilt here; no CI run is published.

Is block sensitivity at most quadratic in spectral sensitivity? (Aaronson, Ben-David, Kothari, Rao and Tal)

What was actually shown

What the AI did

Verification

Sources

Discussion