Gamarnik writes a readable account of the AI proof of the k-SAT threshold

The conjecture says that for each \(k\) there is a fixed clause-to-variable ratio around which the probability that a random \(k\)-SAT formula is satisfiable drops sharply from nearly one to nearly zero. Ding, Sly and Sun settled it for large \(k\) a decade ago with the second moment method; the case of general \(k\) stayed open.

Gamarnik’s note says the conjecture was resolved first by Carenini and shortly afterwards by OpenAI, among some 370 problems its internal model solved, and sets out OpenAI’s argument in a form meant for human readers.