AI Proved What?

Episode 235, October 2026

When does random 3-SAT break?

Four preprints on random k-SAT: another proof that thresholds exist, a square-root window, and a computable 3-SAT threshold

Covers result 235 in OpenAI’s catalog: all 4 papers. See its connections to other results and the work it cites.

Play Episode 235: When does random 3-SAT break? Simulated satisfiability curves sharpening as the number of variables grows.

4:33. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:18The claim
  3. 2:19How the proof goes
  4. 3:40Where it stands

The claim, in plain words

Take n true-or-false variables and add random clauses, each an “or” of three variables with random signs. Each clause vetoes one eighth of all assignments; keep adding until no assignment survives. Experiments show this happens suddenly, and physicists predict it at about 4.27 clauses per variable. But does a sharp threshold density exist as n grows? Chvátal and Reed conjectured it in 1992; Friedgut proved in 1999 that the transition is sharp around some sequence of densities, but not that the sequence converges; Ding, Sly and Sun proved existence for large clause sizes. On October 5, 2026, Gaia Carenini of Cambridge made public a proof for every clause size from three up (ECCC TR26-229).

Result 235 is four OpenAI preprints, 116 pages, dated September 25 to October 5, 2026. They credit Carenini with priority for the threshold’s existence and give another proof for every clause size from three up. Two variance papers claim that the number of clauses at which the formula first becomes unsatisfiable has variance of order n, so the transition window is of order √n clauses; for 3-SAT this is a separate 10-page paper. The fourth claims that the 3-SAT threshold is a computable real number.

What it doesn’t claim

The value of any threshold, or its identification with 4.27; what happens exactly at the threshold; or a rate of convergence. “Computable” means an algorithm exists in principle: it gives no digits, and by our arithmetic from the paper’s explicit constant its error only drops below 0.1 at around 10127 variables.

Where it stands

Posted as preprints
OpenAI, four papers, 116 pages, dated September 25 to October 5, 2026; priority for existence credited to Gaia Carenini (ECCC TR26-229, October 5, 2026)
Peer reviewed
Not yet
Checked in Lean
In part (docs)

Last checked October 19, 2026. The preprints have not been revised since release, and the priority credit was there from the first commit. In Lean, four comparators cover the threshold, the general variance bounds with their sharpness, and computability: about 94,000 lines, much of it a shared spin-glass library; our scan found no unproved steps, and we did not build them. The 10-page 3-SAT variance paper is not formalized, and none of the four papers is in the formalization list. Not among those OSVerify reviewed; we found no expert commentary, only a neutral listing and one outside note that builds on the computability paper.

How the proof goes

  1. Forced variables. A variable is forced if every surviving assignment sets it the same way; a new clause can kill everything only if it hits three forced variables, all with the wrong signs. By a route much like Carenini’s, the threshold paper erases one variable and compares the shortened clauses with full ones, to show forcing adds up slowly. That gives concentration, and a comparison of systems of different sizes shows the centres converge. Carenini reaches concentration and the limit by different steps.
  2. The window. Delete one clause and ask how long the delay lasts. If restoring it kills satisfiability, all its variables are forced, and flipping any one of them must fail. Solution sets that short clauses kill easily die fast under long ones. For 3-SAT a logarithm remained, and the separate paper removes it with a new potential.
  3. Computability. The threshold is bracketed from below by finite computations and from above by finite certificates from spin-glass theory.

The numbers in the video

  • Ours: six variables, clauses added one at a time: after 26 clauses two of 64 assignments survive, after 27 one, with every variable forced; it lasts 21 more clauses until clause 49 contradicts all three of its forced values at once.
  • Ours: our solver (checked against brute force on 360 streams) repeated this for up to 300 variables, about 55,000 times for 3-SAT; the satisfiability curves steepen. The variance of the hitting time divided by n is still falling at 300 variables (12.0 down to 3.1), so small systems neither confirm nor refute the linear law.

Read the source

The 4 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The question

Take n true-or-false variables and add random clauses, each one an or of three variables with random signs. Each clause vetoes 1/8 of all assignments. Keep adding clauses until no assignment survives. Experiments show it happens suddenly; physicists predict it at about 4.27 clauses per variable. But does a sharp threshold density even exist, as n grows? Chvátal and Reed conjectured it in 1992. Friedgut proved in 1999 that the transition is sharp around some sequence of densities, but not that the sequence converges. Ding, Sly and Sun proved existence for large clause sizes, but 3-SAT stayed open. On October 5, 2026, Gaia Carenini of Cambridge made public a proof for every clause size from three up. Here is the game in miniature, with six variables. After 26 clauses only two of 64 assignments survive; after 27, one, with every variable forced. That lone survivor lasts 21 more clauses, until clause 49 contradicts all three of its forced values at once. Our solver repeated this for up to 300 variables, about 55,000 times: the curve of satisfiable probability gets steeper as n grows.

1:18The claim

Result 235 is four OpenAI preprints, 116 pages, dated late September and early October, 2026. They credit Carenini with priority for the threshold’s existence, and give another proof for every clause size from three up. Two variance papers claim that the number of clauses at which the formula first becomes unsatisfiable has variance of order n, so the transition window is on the order of the square root of n clauses; for 3-SAT this is a separate 10-page paper. And the fourth claims that the 3-SAT threshold is a computable real number. Computable here means an algorithm exists in principle; it gives no digits, and its explicit error only drops below a tenth at around 10^127 variables. Not claimed: the value of any threshold, or its identification with 4.27; what happens exactly at the threshold; or a rate of convergence.

2:19How the proof goes

The key quantity is the number of forced variables, those that every surviving assignment sets the same way: a new clause can kill everything only if it hits three forced variables with the wrong signs. By a route much like Carenini’s, the threshold paper erases one variable and compares the shortened clauses with full ones, to show forcing adds up slowly. That gives concentration; a comparison of systems of different sizes then shows the centers converge. Carenini reaches concentration and the limit by different steps. For the variance, delete one clause and ask how long the delay lasts. If restoring it kills satisfiability, all its variables must be forced, and flipping any one of them must fail. Sets of solutions that short clauses kill easily also die fast under long ones. For 3-SAT a logarithm remained, and the separate paper removes it with a new potential. The computability proof brackets the threshold from below by finite computations, and from above by finite certificates from spin-glass theory. In our simulations, the variance divided by n is still falling at 300 variables, from twelve down to about three, so small systems neither confirm nor refute the linear law; it is a large-n statement.

3:40Where it stands

The preprints are unrefereed and unchanged since release. In Lean, four comparators cover the threshold, the general variance bounds with their sharpness, and computability, about 94,000 lines, much of it a shared spin-glass library, with no unproved steps; we did not build them. But the 10-page 3-SAT variance paper is not formalized, and none of the papers is in the formalization list. Not among those OSVerify reviewed; we found no expert commentary, only a neutral listing and one outside note that builds on the computability paper. If they hold, the random 3-SAT threshold, whose existence Carenini proved first in a report, comes with a square-root window and is computable in principle, though no one has computed it.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.