Aftermath bot: New page from public sources: family 176 manuscript, MathVet, cert-machine, con-leche

2026-10-19T21:28:01Z

New page from public sources: family 176 manuscript, MathVet, cert-machine, con-leche

New page

'''The second Kahn–Kalai conjecture''' predicts that the threshold for the random graph ''G''(''n'', ''p'') to contain a fixed graph ''H'' exceeds the graph expectation threshold, the least density at which every subgraph of ''H'' has expected copy count at least one half, by at most a logarithmic factor, uniformly in ''H''. A manuscript in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 24 September 2026, claims the conjecture with a factor of order 1 + log2 ''h'', where ''h'' is the number of edges of ''H''. The collection includes a Lean formalization of the theorem. 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:
** Kahn and Kalai conjectured the comparison. For a perfect matching or a Hamilton cycle the containment threshold exceeds the expectation threshold by a logarithmic factor, so a logarithm is necessary.
** For abstract increasing families, Frankston, Kahn, Narayanan and Park proved the fractional bound and Park and Pham the integral bound; for graph containment these give the expectation threshold of the covers, not the graph expectation threshold. Mossel, Niles-Weed, Sun and Zadik obtained a single logarithm for a modified graph threshold.
** Dubroff, Kahn and Park proved a bound with loss log2 ''n'' for the comparison of expectation thresholds, and further special cases, and Tran ([https://arxiv.org/abs/2609.20546 arXiv:2609.20546]) reduced the general containment loss to the square of a logarithm and proved the conjecture for trees and for graphs whose average degree is at least the logarithm of their maximum degree. The manuscript uses Tran's ratio-maximizing cores and addresses a coupling question he raised.

== The original result ==
* '''Claim.''' Theorem 1.1 of ''The second Kahn–Kalai conjecture'' states that for every ''n'' ≥ 2 and every finite simple graph ''H'' with ''h'' ≥ 1 edges and at most ''n'' vertices, the containment threshold is at most min{1, 2048·e50·''p''E(''n'', ''H'')·(1 + log2 ''h'')}, and in particular at most 6144·e50·''p''E(''n'', ''H'')·log2 ''n''; the graph ''H'' may vary with ''n''.
* ''Method, as described:'' starting from an edge subset, one chooses the subgraph that maximizes a weighted probability of lying in a uniform copy, following Tran's cores, and the required containment bound is proved through a tree reduction that keeps all possible extension histories and reduces every level with the same random set.
* '''Source.''' The manuscript [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-second-Kahn-Kalai-conjecture-September-24-2026 The second Kahn–Kalai conjecture] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/176.md scope note] states that the formalization proves the comparison up to a universal factor times 1 + log2|''E''(''H'')|, and hence up to a universal factor times log2 ''n'', for every graph with at least one edge and at most ''n'' vertices, ''n'' ≥ 2, using the actual containment and expectation thresholds. The Comparator statement is <code>SecondKahnKalai.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": the Lean statement gives both bounds with the explicit constants, with the containment threshold defined through Mathlib's copy counts and the expectation threshold over all subgraphs, matching the summary's definition. It records a sandboxed Comparator pass for <code>SecondKahnKalai</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/a4925f1fde8ec8ab8152e58e8c32961741ed6016/corpus/openai-math/kernel-runs/38019899278/SecondKahnKalai.json cert-machine], openai/math lane K, run 38019899278 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>SecondKahnKalai</code> solution (67 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>SecondKahnKalai</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|}

== Notes ==
* The earlier results are due to the authors named in the Background section, as recounted by the manuscript; Tran's preprint precedes 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 second Kahn–Kalai conjecture - Revision history

Aftermath bot: New page from public sources: family 176 manuscript, MathVet, cert-machine, con-leche