The Gopalan–Servedio square-root degree conjecture

The Gopalan–Servedio square-root degree conjecture asks whether the sum of the linear (level-one) Fourier coefficients of a Boolean function f : {−1, 1}ⁿ → {−1, 1} is at most a constant times the square root of its degree. By the Cauchy–Schwarz inequality the sum is at most √n, and the conjecture proposes √deg(f) in place of √n. A manuscript dated 26 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims that no constant multiple of the square-root bound holds, and the collection includes a Lean formalization of the main statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • The conjecture is attributed to Gopalan and Servedio, around 2009, in O'Donnell's problem list, and it appears as Conjecture 3.17 in a preprint of Filmus, Hatami, Keller and Lifshitz. The universal signed and absolute-value versions are equivalent, since changing the signs of coordinates preserves the degree.
  • A sharper proposal in the same problem list replaces √d by the singleton sum of majority on d bits. Jha and Wang gave reformulations, Wang proved the cases d = 1 and d = n − 1, and Kudin and Pašalić proved the cases d = 2, 3 and refuted the majority version at d = 4. A counterexample to the majority version need not violate the square-root bound.
  • A linear bound holds for every Boolean function: the sum of the absolute values of the linear coefficients is at most the total influence, which is at most the degree (Nisan and Szegedy).
  • Square-root bounds hold in decision-tree settings: O'Donnell and Servedio bound the singleton sum by the square root of the expected depth of a decision tree, and Blais, Tan and Wan prove such bounds in terms of parity decision-tree depth.

The original result

• Claim. Theorem 1.1 of Unbounded Violations of the Square-Root Degree Bound states that for every real C > 0 there are an integer n and a nonconstant Boolean function f on {−1, 1}ⁿ whose linear Fourier coefficients sum to more than C√deg(f). Consequently the ratio of the sum of their absolute values to √deg(f) is unbounded. The manuscript states that the dimension and copy counts in the construction are finite but that it does not obtain useful bounds on their growth.
• Method, as described: the proof first builds finite observations F of independent signs and compares the variance v(F) of the conditional expectation of the coordinate sum given F with the largest degree of an indicator of a cell of F. A reporting rule on m + 1 asymptotically normal scores, which reports a single tag on an exceptional event, retains more than m units of variance at degree cost m. Independent copies and the central limit theorem amplify this gain, and a final sign readout gives the Boolean function.
• Sources. Commit 1581d4c of the openai/math repository, folder Unbounded Violations of the Square-Root Degree Bound.
• Formalization, as described by the repository. The scope note states that the formalization disproves the conjecture by an unbounded factor, giving for every C > 0 a nonconstant Boolean function on a finite sign cube whose linear Fourier coefficients sum to more than C√deg(f), with the real multilinear degree, and that it also proves the unboundedness of the absolute-value ratio. The Comparator statement is SquareRootDegree.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 26 October 2026)
2026-10-07 (manuscript 04 added 9 October 2026)	ProveIt project, square-root degree bound (GitHub repository VladimirReshetnikov/ProveIt, commit 16ecdd6)	Extension (thresholds, explicit witness, quantitative amplifier)	A merged report of four manuscripts on the manuscript's observation framework. The main manuscript, Sharp Codimension Thresholds and Uniform Amplification on the Boolean Cube, proves that the retained variance is at least the degree cost whenever every cell has degree at most N − k with k = 1, 2, 3, with equality cases and stability. At k = 4 it gives an explicit partition of the twenty-dimensional cube into 622 cells of degree 16 whose retained variance is 16 + 9/34816, certified in exact rational arithmetic and minimal in twenty bits within a stated reporting family. It quantifies the normal-approximation amplifier with one averaging count at every stage and a positive, extremely small explicit power exponent.	The README describes the four manuscripts as AI-assisted, unrefereed and not formalized; the main manuscript, dated 7 October 2026, states that it was generated with ChatGPT (GPT-6 Astra Pro). The README notes that a later manuscript in the report re-derives the same twenty-bit example without citing the first.
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit 899d421, 25 October 2026)	Review (fidelity of the formal statements)	Rates this family "full" and records a sandboxed Comparator pass for SquareRootDegree. Its note states that the Fourier coefficients and the degree are the standard ones and that the formal statement matches the collection's summary.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-08 (supplements added 17 October 2026)	Pico, row 192 in piiiico/openai-math-counterexamples, with supplements by A. R. Towell	Verification (finite checks)	The row notes that the manuscript gives no explicit function, and an exhaustive search over all Boolean functions on at most four variables finds a ratio of at most 1, so a witness for C ≥ 1 needs at least five variables. A. R. Towell (GitHub user queelius) added exact scalar certificates for rational Gaussian reporting parameters, a single finite-sign transfer stage and recursive amplification budgets; no explicit Boolean witness is evaluated.	GitHub repository maintained by an AI agent; the row's result is “not-explicit”, which the repository defines as: the paper proves the object exists but never writes it down. The supplements were prepared with OpenAI Codex assistance and are not formally verified.
2026-10-09	The square-root degree bound, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public)	Reading (exposition)	Four lessons with proofs, examples and exercises with solutions, covering linear Fourier coefficients and degree, asymptotically normal scores, the tagged report and average degree costs.	The course states that it was written and self-checked by Claude Opus 5.5 (Anthropic) and that independent review is not complete.
2026-10-10	cert-machine, openai/math lane K: run 38019899278 for SquareRootDegree	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the solution, in 230 s.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list SquareRootDegree, so the challenge was accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap after reading the main file and Sections 0–2 in full, which the manuscript says contain the complete proof. Its one minor note is quantitative: the central Gaussian estimate in Lemma 2.2 tends to zero only for astronomically large m, which the reviewer says does not affect the argument because only some finite m is needed.	Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.