A finite range where the SubexponentialSAT bound's exponential factor sits above 2^n with A = 1, and the receipt of a comparator rerun

Two checkable things about the SubexponentialSAT challenge of openai/math. The first is the receipt of a rerun of leanprover's comparator on the published solution, carried out under a real sandbox on 2026-10-28, with the provenance needed to repeat it and the raw log of all three runs, the two earlier failures included. Those two were failures of the preparation script rather than verdicts on the proof, and the receipt says so at the top rather than leaving it to be discovered. Three limits of the run are stated in the same place: it used Lean's default kernel, so it is a rerun and not a check by a second kernel implementation; the recorded commit identifies the comparator source rather than the binary executed; and a comparator result says nothing about whether a formal statement means what the informal claim says.

The second is a recomputation of the stated time bound, T <= C (bits+1)^d 2^(A runtimeScale(n)) with runtimeScale(n) = n ln(ln(n+16))^2 / sqrt(ln(n+16)). Dividing by n leaves ln(L)^2 / sqrt(L) with L = ln(n+16), which tends to zero, so the exponent is o(n). What the asymptotics do not show is that this ratio is not monotone: it starts below 1, rises to a maximum of 16/e^2 at L = e^4, and falls back. Stipulating A = 1, it crosses 1 twice, and both crossings are closed-form in the Lambert W function through L = exp(-4 W(-1/4)), on the two real branches: ascending at n = 49.175096 and descending near 10^2390.21. Since n counts variables, the range runs from n = 50 upward.

What this does not establish matters as much as what it does. An upper bound above 2^n says nothing about running time, because the algorithm may run far below its own bound; the comparison here is between bounds. The exponent is o(n) for any fixed A, so a finite range cannot bear on an asymptotic statement, and nothing here refutes anything. The constant A is existential in the statement and is not determined by it: below A = e^2/16, roughly 0.46, the exponential factor stays under 2^n for every n at least 1, so A = 1 is a stipulation made to have something concrete to compute, not a value anyone has established. Two further conditions are left open and are claimed nowhere: that the formal statement is a faithful rendering of k-SAT, and that the unary encoding keeps the input size polynomial.

The arithmetic reproduces in seconds with nothing beyond the Python standard library, and a plant mode corrupts the transcribed formula and requires the self-tests to reject it. The comparator run is a different matter: it took 3 h 47 min over 12,014 build jobs and needs a Linux host with Lean, elan and landrun, so for most readers the receipt and the raw log are the practical object rather than a rerun of the rerun.