Lean Replications

I reran both Lean proofs locally, under the comparator, and both are accepted. The receipts, the raw logs and the scripts are in two places. The repository:

https://github.com/totobusnello/eth-subexp-note

and the archived version, where v1.1.0 is the first to carry both runs:

https://doi.org/10.5281/zenodo.23820111

The openAI proof (SubexponentialSAT). On 2026-10-28 the comparator from leanprover/comparator, under the landrun sandbox, reported that the Lean kernel accepts the solution for the challenge’s own declaration, OAI.Algorithms.SubexponentialSAT.SqrtLogSpace.exact_count_and_sat. Of the declarations that print their own axiom dependencies, 19 in total, every one declares exactly the three permitted axioms, propext, Classical.choice and Quot.sound. Three limits of that run: it used Lean’s default kernel, so it is not an independent check from a second kernel implementation, because that challenge sets enable_nanoda to false; the recorded commit identifies the comparator source rather than the binary I executed; and a comparator result says nothing about whether the formal statement means what the informal claim says.

The Anthropic proof. On 2026-10-30 I ran the fuller check that their own CI runs, and it closes the first of those three limits, because their comparator.json sets enable_nanoda to true. The log reads, in this order: “Running nanoda kernel on solution”, “nanoda kernel accepts the solution”, “Running Lean default kernel on solution.”, “Lean default kernel accepts the solution”, “Your solution is okay!”, “All 1 comparator configuration(s) accepted.”

So two independently written kernels accept that proof, and the comparator also checks the Solution theorems against the trusted Challenge statements. Both of the declarations the challenge names, MainResults.ethIsFalse and MainResults.mainTheorem, print the same three standard axioms and nothing else. The two “declaration uses sorry” warnings are the ones their README predicts, both from Challenge.lean, which states the two theorems without proofs so that the comparator has something trusted to compare against.

Now the part no machine did. A comparator result is about proofs, not about meaning, and their README says the same about their own file: “no machine checks that this file says what the paper says; the file is kept short so that a reader can check this”.

So I read both statements by hand, and the second is much cheaper to read than the first, by their design: Challenge.lean is 17 lines and imports MainResults.lean alone, which is 182 lines of definitions with no theorem and no proof, importing Mathlib alone. For the openAI statement I reported four checks, one of which I could not complete: the encoding is unary and I did not establish what that costs in length. For the Anthropic statement I report six, and one of them closes that same question for their formalization: encClauses writes the variable count n in unary but each clause as k positions of floor(log2 2n) + 1 bits, which is binary, so the input is about n + 1 + mk(floor(log2 2n) + 1) bits, polynomial in n and m. Another is that both their statements require every stack alphabet to be finite, where Mathlib requires only the input stack’s, which makes the claim harder rather than easier.

Two things I did not do, and they are where another reader is most useful. I did not read either proof development; that is what the kernels checked, and the division of labour here is kernels for the proof, a human for the statement. And I did not compare their formal statement against their paper, which I have not read: reading a statement and checking it against a paper are different jobs, and only the first is done. On that second job their own file is unusually forthcoming about where it stops. Its head comment argues that a random-access machine simulates their machine type with bounded overhead and that renaming variables is polynomial, so that s3 = 0 in their sense gives s3 = 0 in the usual sense, and then says: “The simulation and the rewriting are standard facts; they are not part of the Lean statements or proofs”. So the kernels certify a theorem about Mathlib’s machine type, and the step from there to the hypothesis as complexity theory states it is prose. Naming which step sits outside Lean is more than the openAI challenge does, and it is the right place for a further pair of eyes.

Separately, an arithmetic note on the openAI bound, which is reproducible in seconds. The stated bound is T <= C * (bits+1)^d * 2^(A * runtimeScale(n)), where runtimeScale(n) = n * ln(ln(n+16))^2 / sqrt(ln(n+16)), with C, A and d existential. Setting A to 1, the ratio runtimeScale(n)/n is not monotone: it starts below 1, rises to a maximum of 16/e^2 at L = e^4, and falls back. It crosses 1 twice, and both crossings are closed-form in the Lambert W function via L = exp(-4 W(-1/4)) with L = ln(n+16): ascending at n = 49.175096 on the principal branch, descending near 10^2390.21 on branch -1. Over that finite range the exponential factor sits above 2^n.

Two things that do not follow from it. A = 1 is a stipulation, not a determined value: the statement does not fix A, and below roughly e^2/16 the exponential factor stays under 2^n for every n. And an upper bound above 2^n is not a statement about running time, since the algorithm may run far below its own bound; the comparison is between bounds. The exponent is o(n) for any fixed A, so a finite range cannot bear on an asymptotic claim. This refutes nothing.

Provenance for the openAI run, for anyone who wants to repeat it. Clone openai/math at 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a. Challenge json sha256 debbfdc9c01104d2369be80da5180978275106df8b685f693fba7ce7da7c5b19. Challenge lean sha256 4183b2057cff350d66848215ff7167196dfc20e1891b598fdddea59077a76685. Toolchain leanprover/lean4:v4.34.1. Comparator leanprover/comparator at 865edc14486c3388e9225daa971da8e157488c3e. Lean4export 5a9a355dc6c5fd82b69058d433e2ae2e8dfbf8fe, landrun 0.1.18. Cost 3 h 47 min for the verdict step, over 12,014 build jobs.

Provenance for the Anthropic run. Clone anthropics/formal-math at 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. Comparator.json sha256 757e5537ccf47d1946521b0b5fb91a230cdcfd8933dc9ab047710709c15ffa7e. Challenge.lean sha256 63f54edafad0b4d1a4184c6279dc2fea4d8b3a6ef39fa04ab7fa72e86bfbb39e. Solution.lean sha256 27d304798a6ec294db7fdeee301227b70d72044cb31c85615901a8d728b0b98f. Toolchain leanprover/lean4:v4.33.1. Nanoda 68d5ca9db226849b41a6fff59d796ff19d0a8840, landrun 811cfff51ceaf3d9843708aa6d22e9b84ccac8b4. Cost 42 min 28 s of wall clock on five cores.

On the practical side, for the “how do we do this systematically” half of the thread: the two runs cost different amounts. The openAI check took 3 h 47 min over 12,014 build jobs; the Anthropic one took 42 minutes on five cores, of which 28 were the Lean build and 10 were building nanoda and landrun from their pinned commits. Neither needs special hardware, but both need a Linux host, because landrun does. The arithmetic note needs nothing but a Python interpreter, and its script runs eight self-tests before printing any number.

Totó Busnello