The Friedgut–Kalai sharp-threshold conjecture

The Friedgut–Kalai sharp-threshold conjecture asks how quickly a symmetric increasing property of the random graph switches from unlikely to likely as the edge probability grows: Friedgut and Kalai proved a transition width of order 1/log n and conjectured 1/(log n)², with an analogous exponent for uniform hypergraphs. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September and 5 October 2026, claim proofs of the graph and hypergraph conjectures. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.

Background

• As recounted in the introductions of the manuscripts:
  • The influence theorem of Kahn, Kalai and Linial connected Fourier analysis with the sensitivity of Boolean functions to single coordinates, and Bourgain, Kahn, Kalai, Katznelson and Linial extended it to product spaces. Friedgut and Kalai combined this with the Margulis–Russo identity: every increasing family invariant under a transitive group of coordinates has a narrow transition, and for graph properties on n vertices the width between probabilities ε and 1 − ε is at most C log(1/(2ε))/log n. They conjectured the denominator (log n)², which is the optimal order, as the property of containing a clique of order proportional to log n shows, and an exponent r/(r − 1) for r-uniform hypergraph properties.
  • Bourgain and Kalai, using the action of the symmetry group on sets of coordinates, obtained the width (log n)^−2+η for every η > 0.

The original results

• Graphs. Theorem 1.1 of A Sharp Threshold Bound for Monotone Graph Properties states that for every n ≥ 2, every nontrivial increasing family of graphs on n vertices invariant under all vertex permutations, and every 0 < ε < 1/2, the edge probabilities at which the family has probability ε and 1 − ε differ by at most 2¹⁹ log(1/(2ε))/(log n)². The manuscript calls the constant only a convenient explicit choice. It derives the theorem from a variance bound, Var_p(f) ≤ 2¹⁷ I_p(f)/(log n)² for every graph property f and every p, where I_p is the total influence; no monotonicity is assumed there.
• Hypergraphs. Theorem 1.1 of A uniform influence bound for hypergraph properties states that for every r ≥ 3 there is a constant C_r such that every property f of r-uniform hypergraphs on n vertices satisfies Var_p(f) ≤ C_r I_p(f)/(log n)^r/(r−1) for all 0 < p < 1, without a monotonicity assumption. A corollary gives the conjectured threshold width for increasing hypergraph properties.
• Method, as described: biased Fourier analysis with hypercontractivity, restriction of a symmetric function to the edges that meet a random block of vertices, and an argument that captures each Fourier support at one vertex; the hypergraph manuscript states that it reproduces the graph manuscript's Fourier estimate and vertex-block restriction and replaces the degree estimate by an r-uniform one.
• Sources (openai/math repository, commit 7ef5c0c):
  • A Sharp Threshold Bound for Monotone Graph Properties (25 September 2026);
  • A uniform influence bound for hypergraph properties (5 October 2026).
• Formalization, as described by the repository. The scope note lean/docs/186.md concerns the graph manuscript: it states that the formalization proves the width bound 2¹⁹ log(1/(2ε))/(log n)², uniformly over the property, n and ε. The Comparator statement is SharpThreshold.lean. The hypergraph manuscript has no formalization.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 29 October 2026)
2026-10-07	G. Kalai, Updates: Sharing AI progress on mathematics (amazing!); and my lecture plans, a post on the blog Combinatorics and more	Remark (blog post)	One of the conjecture's two authors lists the result among connections between the release and earlier posts of his blog: sharp thresholds and the role of symmetry were central themes of his earlier post on influence, thresholds and noise, and the release announces the threshold-width bound for monotone graph properties together with the conjectured extension to uniform hypergraphs.	Blog post of 7 October 2026. The post states that the collection includes results at different stages of verification, that their proofs will need to be checked and digested by the mathematical community, and that even Lean verification may have issues.
2026-10-07	Influence and symmetric threshold widths, an article of the Latent Seminar blog at lowrank.github.io	Reading (exposition)	Explains threshold location and transition width, pivotal influences and the two claims, the integration of the influence inequality, Fourier mass and surviving symmetry, and the passage from low to higher degrees, with proof outlines of the derivative, conditioning and vertex-capture steps.	Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs.
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026)	Review (fidelity of the formal statements)	Rates this family "partial": only the graph case is stated in Lean, while the hypergraph width and the nonmonotone influence bound named in the collection's summary have no formal statement. It records a sandboxed Comparator pass for SharpThreshold.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-09	Sharp thresholds for graph properties, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public)	Reading (exposition)	Three lessons: biased Fourier analysis and hypercontractivity, vertex blocks and graph properties, and hypergraph properties.	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	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the SharpThreshold solution, in 170 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 does not list SharpThreshold, so it was accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee reviews rank_510 (graph manuscript) and rank_534 (hypergraph manuscript) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap and no minor notes for either manuscript.	Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
2026-10-16	AI Proved What?, episode 186 How fast must it switch?, remade version of 24 October 2026	Reading (exposition)	Video explainer of both claims, with the history from Kahn, Kalai and Linial to Bourgain and Kalai. The episode states that the result is not a useful numerical bound: by its own arithmetic the graph width bound beats the trivial width 1 at ε = 0.1 only for n above about 10398.9, and the content is the rate in n. It also observes that the width is measured in the edge probability itself, so it says nothing new for properties that switch close to probability zero, such as connectivity.	Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as preprints: OpenAI, graph paper 10 pages, September 25, 2026, hypergraph paper 8 pages, October 5, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the graph theorem, exactly as stated, formalized by OpenAI and not run by the site; the hypergraph paper has no Lean. The page states that it found no unproved steps by search in the 78 files of the graph formalization without rebuilding it.

Notes

• The background summarizes the manuscripts' own account of earlier work.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.