---
id: "2026-10-05-random-k-sat-satisfiability-conjecture-carenini-openai"
url: "https://postcutoff.com/e/2026-10-05-random-k-sat-satisfiability-conjecture-carenini-openai/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-05"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Peer-reviewed
sources: 8
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-05-random-k-sat-satisfiability-conjecture-carenini-openai/

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

Full title: The satisfiability conjecture for random k-SAT claimed for every k ≥ 3: Gaia Carenini's human-written proof on ECCC (5 Oct) and an alternative OpenAI proof with an accepted Lean statement (6 Oct release) that credits her with priority

Gaia Carenini, "A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture" (ECCC TR26-229, 5 Oct 2026): the scaling window has width O(n^{1/2+1/k}), which with a result of Abbe and Montanari gives a limiting threshold α_k for every fixed k ≥ 3. Its AI statement reads "None of the mathematical arguments in this paper was generated by a large language model." OpenAI's 6 Oct release (family 235) proves the same existence statement differently ("A Limiting Satisfiability Threshold for Every Fixed Clause Size", dated 25 Sept), plus Var(H_n) = Θ_k(n) for the first unsatisfiable prefix (k ≥ 4, and k = 3 in a companion paper) and computability of the 3-SAT threshold. OpenAI credits Carenini with priority. Lean statements for all four results were accepted by oai-math-revised's Comparator run of 26 Oct.

## 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

## What happened

Random k-SAT asks whether a formula of ⌊αn⌋ random k-clauses on n variables can be satisfied. Experiments in the early 1990s showed a
sharp change at a critical density (Mitchell, Selman and Levesque, 1992). The conjecture that this happens at one limiting density α_k has been a
benchmark problem for probabilists, computer scientists and statistical physicists since. Friedgut proved in 1999 that the transition is
sharp, but not that its location converges. Ding, Sly and Sun settled the question for large k in 2022.

On 5 Oct Gaia Carenini, a PhD student at Cambridge, posted a short ECCC report. She narrows the scaling window to a polynomially small
width and combines this with a 2014 result of Abbe and Montanari to get the conjecture for every fixed k ≥ 3. Her report says no part of
the argument came from a language model. A day later OpenAI released its maths papers. Family 235 contains a different proof of the same
statement, dated 25 Sept, together with results on the variance of the hitting time and the computability of α_3. OpenAI's catalogue
credits Carenini with priority. The Lean statements of all four OpenAI results were accepted in the community's Comparator re-run.

## Why it matters

If either proof holds, a central conjecture about phase transitions in random computational problems is settled for every clause size,
including the k = 3 case that motivated the field. This is also a rare priority case in OpenAI's release that OpenAI itself resolved in
favour of a human, apparently AI-free proof. The machine-checked OpenAI statement makes the existence claim the easier of the two to audit,
provided the formal random model is the standard one.

## What is disputed or not yet verified

- Verification: Carenini: unrefereed ECCC report. OpenAI: unrefereed manuscripts with Lean statements accepted by the community Comparator run (26 Oct)

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 158 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 97 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 188 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 127 days after its cutoff

## Sources

1. [ECCC TR26-229: A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture (Carenini)](https://eccc.weizmann.ac.il/report/2026/229/) (eccc.weizmann.ac.il, paper)
2. [OpenAI: A Limiting Satisfiability Threshold for Every Fixed Clause Size (25 Sept 2026, PDF)](https://github.com/openai/math/blob/main/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf) (github.com, paper)
3. [OpenAI: Computing the Random 3-SAT Threshold (27 Sept 2026, PDF)](https://github.com/openai/math/blob/main/preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf) (github.com, paper)
4. [OpenAI: Linear Variance of the Random 3-SAT Hitting Time (5 Oct 2026, PDF)](https://github.com/openai/math/blob/main/preprints/Linear-Variance-of-the-Random-3-SAT-Hitting-Time-October-5-2026/linear-variance-of-the-random-3-sat-hitting-time.pdf) (github.com, paper)
5. [openai/math lean/docs/235.md: scope of the Lean formalization](https://github.com/openai/math/blob/main/lean/docs/235.md) (github.com, code)
6. [oai-math-revised Comparator run, 26 Oct (results.tsv)](https://github.com/mathcommunity/oai-math-revised/blob/main/checks/comparator-2026-10-26/results.tsv) (github.com, code)
7. [arXiv 2609.26222: The Scaling Window of Random k-SAT (Carenini, August)](https://arxiv.org/abs/2609.26222) (arxiv.org, paper)
8. [Background: Ding, Sly, Sun, Proof of the satisfiability conjecture for large k (Annals of Mathematics, 2022)](https://annals.math.princeton.edu/2022/196-1/p01) (annals.math.princeton.edu, paper)

## Changes

- 2026-10-29 (filed): Created (ECCC report page and PDF, oai-math-revised Comparator results, arXiv author listing, web and HN search)

## Related

- 2026-10-26: [OpenAI claims ETH is false](https://postcutoff.com/e/2026-10-26-openai-eth-false-subexponential-sat-claim/index.md)
- 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)