Random k-SAT threshold exists for every k ≥ 3: a human proof and an OpenAI Lean-checked proof

Your AI and this story

Key facts

• Carenini abstract (ECCC TR26-229, posted 5 Oct, 1,346 downloads by 29 Oct): ‘We prove that the scaling window of random k-SAT has width O(n^{1/2+1/k}), a polynomial improvement over our previous bound of O(n/log n). Combined with a result of Abbe and Montanari, this establishes the satisfiability conjecture for every fixed k ≥ 3.’ The O(n/log n) bound is her August preprint ‘The Scaling Window of Random k-SAT’ (arXiv 2609.26222)
• Carenini’s AI statement (verbatim): ‘Statement regarding artificial intelligence. None of the mathematical arguments in this paper was generated by a large language model.’ She thanks Imre Leader; affiliation University of Cambridge (Trinity College studentship)
• OpenAI family 235 (CONTENTS.md, verbatim): ‘We credit Gaia Carenini with priority for resolving the threshold-existence conjecture in her concurrent ECCC TR26-229, made public October 5, 2026; this family supplies another proof and the sharper variance and computability results.’ The first paper’s own abstract calls its argument ‘an alternative proof, using concentration of a capped last satisfiable index and a comparison between different system sizes’
• Lean scope (lean/docs/235.md): ‘The formalization proves that every fixed integer k ≥ 3 has a finite positive threshold α_k … The statement makes no assertion at the threshold itself’; clauses use distinct variables with uniform signs, sampled independently with replacement. It also covers Var(H_n) = Θ_k(n) for k ≥ 4 (O(n log n) upper bound for k = 3 in Lean) and that α_3 is ‘a computable positive real’
• Community check: FixedClauseThreshold, SATSharpness, SATVariance and SATComputability are all ‘accepted’ in mathcommunity/oai-math-revised checks/comparator-2026-10-26/results.tsv. Acceptance means the proof checks against the challenge statement. It does not show that the formal model matches the usual random k-SAT model in every detail
• Prior state: Friedgut’s sharp-threshold theorem (1999, with Bourgain’s appendix) gives a threshold sequence α_k(n) without proving convergence; Ding, Sly and Sun proved the conjecture and the 1RSB value for large k (Annals of Mathematics 196, 2022). For k = 3 neither the existence nor the value of the limit was known before October
• Not determined: the numerical value of α_3; OpenAI’s computability result says it can be approximated to any precision by one deterministic machine, without a rate
• Reactions: none found as of 29 Oct (web, Hacker News, ECCC comments); random-graph and statistical-physics experts (Sly, Coja-Oghlan, Perkins, Achlioptas) have not commented publicly that we could find