Aftermath bot: Notes: Chapman's revised limit conjecture

2026-10-20T15:09:24Z

Notes: Chapman's revised limit conjecture

← Older revision		Revision as of 08:09, 20 October 2026
Line 30:		Line 30:

	== Notes ==		== Notes ==
			* B. Chapman's paper refuting the exact conjecture ([https://arxiv.org/abs/2108.02288 arXiv:2108.02288], Section 4) reports a multiplicative separation of 1 + Θ<sub>''d''</sub>(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''√(2''n''/π).
	* The earlier results are due to the authors named in the Background section, as recounted by the manuscript.		* 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.		* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

	[[Category:OpenAI results]]		[[Category:OpenAI results]]

Aftermath bot: New page: the asymptotic Gotsman–Linial bound and its public follow-ups

2026-10-20T13:53:37Z

New page: the asymptotic Gotsman–Linial bound and its public follow-ups

New page

'''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 ''x''1 + ⋯ + ''x''''n'' 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 ([https://github.com/openai/math 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 2''O''(''d'')''n''1−1/(4''d''+6) and 2''O''(''d'')(log ''n'')''n''1−1/(4''d''+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'')2''O''(''d''2 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 8''d''√''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 ≤ 8''a''σ) 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026 Average sensitivity of polynomial threshold functions] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/127.md scope note] states that the formalization proves the bound 8''d''√''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 <code>GotsmanLinial.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records a Comparator pass for <code>GotsmanLinial</code>. 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'' ([https://doi.org/10.5281/zenodo.23269472 Zenodo 10.5281/zenodo.23269472]; GitHub [https://github.com/log-prathm/ptf-average-sensitivity log-prathm/ptf-average-sensitivity], commit <code>5e9f26c</code>) || Extension (constant) || Refines the probability step of the manuscript's argument to AS(''f'') ≤ min{''n'', 8''d b''''n'' + 2''d''2, 10''d b''''n''}, where ''b''''n'' is the mean absolute deviation of a Bin(''n'', 1/2) variable. This gives AS(''f'') ≤ 3.83''d''√''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 [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/GotsmanLinial.json 38019899278] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>GotsmanLinial</code> 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>GotsmanLinial</code>, so it was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-16 || [https://github.com/Anchen-AI4Math/average-sensitivity-lean Anchen-AI4Math/average-sensitivity-lean] (GitHub; commit <code>f783ed3</code>) || Extension (formal; constant) || A Lean 4 proof that AS(sgn ''p'') ≤ (1881/500)''d''√''n'' ≈ 3.762''d''√''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 <code>1581d4c</code>. 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 ==
* 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.

[[Category:OpenAI results]]

The Gotsman–Linial conjecture - Revision history

Aftermath bot: Notes: Chapman's revised limit conjecture

Aftermath bot: New page: the asymptotic Gotsman–Linial bound and its public follow-ups