The Gotsman–Linial conjecture
From OpenAI Aftermath
The Gotsman–Linial conjecture concerns the average sensitivity, or total influence, of polynomial threshold functions: Boolean functions f = sgn(p) on the cube {−1, 1}n given by a real polynomial p of degree at most d. Gotsman and Linial (1994) proposed that a symmetric function, the sign of a degree-d polynomial in x1 + ⋯ + xn whose roots lie between the central levels of the cube, has the largest average sensitivity; that value is of order d√n. The exact form of this proposal is false, and its asymptotic form asks for the bound O(d√n). A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the asymptotic form with the constant 8, and the collection includes a Lean formalization of this bound. 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:
- Chapman constructed counterexamples to the exact extremal assertion and explicitly distinguished it from the asymptotic bound O(d√n). Kim, Maldonado and Wellens independently constructed quadratic counterexamples for odd n ≥ 5 and proved influence bounds for quadratic polynomials with restricted support graphs.
- The symmetric examples attain the order d√n whenever d ≤ √n, and every Boolean function has average sensitivity at most n.
- Harsha, Klivans and Meka, and independently Diakonikolas, Raghavendra, Servedio and Tan, proved sublinear bounds for every fixed degree, of the forms 2O(d)n1−1/(4d+6) and 2O(d)(log n)n1−1/(4d+2); both first circulated in 2009. Kane reached the square-root exponent in the dimension with a polylogarithmic loss, √n(log n)O(d log d)2O(d2 log d).
- Chang, Slote, Volberg and Zhang bounded the Boolean surface area for each fixed degree, and Tseng and Volberg studied further moments of the local sensitivity; at the first moment, the resulting influence bounds keep a logarithmic factor.
The original result
- Claim. Theorem 1.1 of Average sensitivity of polynomial threshold functions states that for all integers n ≥ 1 and 1 ≤ d ≤ n and every real multilinear polynomial p of degree at most d, the function f = sgn(p), with sgn(0) = 1, has average sensitivity at most 8d√n. The constant depends on neither d nor n, the polynomial may vanish on the cube, and no regularity condition is imposed. The manuscript makes no assertion about exact maximizers. Its corollaries give a noise-sensitivity bound NSη(f) ≤ Cd√η for 0 < η ≤ 1/2 and an agnostic learning guarantee for labeled samples whose input marginal is uniform.
- Method, as described: a coupling estimate (equal-law random variables U, V of variance σ2 with V − U ≤ a satisfy E(U − V)2 ≤ 8aσ) is combined with a self-adjoint operator defined by grading the cube polynomials by degree in a weighted inner product, with weight |p|. Multiplying f by the full parity turns its sensitive edges into equal-sign edges, whose number is bounded through an anticommutator with the sign operator; the parity shift of the Fourier support of p supplies a coupling of two binomial laws with V − U ≤ d.
- Sources. The manuscript Average sensitivity of polynomial threshold functions at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves the bound 8d√n for every Boolean threshold function defined by a real multilinear polynomial of degree at most d on the n-dimensional cube. The Comparator statement is
GotsmanLinial.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records a Comparator pass for GotsmanLinial. Its note states that the exact-extremizer form of the Gotsman–Linial conjecture is not claimed. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 | P. Lagdive, V. Aglave, S. Damre, An elementary improvement of the average sensitivity bound for polynomial threshold functions (Zenodo 10.5281/zenodo.23269472; GitHub log-prathm/ptf-average-sensitivity, commit 5e9f26c) |
Extension (constant) | Refines the probability step of the manuscript's argument to AS(f) ≤ min{n, 8d bn + 2d2, 10d bn}, where bn is the mean absolute deviation of a Bin(n, 1/2) variable. This gives AS(f) ≤ 3.83d√n uniformly, and the coefficient 8/√(2π) as d/√n → 0. The weighted grading and edge recovery are attributed to OpenAI. | Derivation and review used OpenAI Codex; exact finite checks accompany the analytic proof. No independent human review or Lean formalization; optimality and exhaustive priority not claimed. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the GotsmanLinial solution, in 88 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
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 GotsmanLinial, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | Anchen-AI4Math/average-sensitivity-lean (GitHub; commit f783ed3) |
Extension (formal; constant) | A Lean 4 proof that AS(sgn p) ≤ (1881/500)d√n ≈ 3.762d√n for every real polynomial p of degree at most d. It formalizes the coupling refinement of Lagdive, Aglave and Damre (row above), extracts a sharper uniform constant, and builds on the collection's Lean development at commit 1581d4c. The repository reports only the standard axioms and three accepted components on the Prove2Me platform. |
Codex-assisted; no independent human review claimed; no optimality or exhaustive priority claim. |
Notes
- B. Chapman's paper refuting the exact conjecture (arXiv:2108.02288, Section 4) reports a multiplicative separation of 1 + Θd(1/n) for its counterexamples and proposes a revised "limit" conjecture: every degree-d polynomial threshold function on n variables has average sensitivity at most d times that of the majority function, which is about d√(2n/π).
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
