Three of today’s items turned out to be about one question, which is what a proof or a signal actually certifies, and how wide the gap is between that and what you assume it certifies. Then one small, happy piece of assembly to end on.

The ETH disproof, and what Lean does and does not check

OpenAI announced that its models produced three research results, and the one that matters most is a claimed disproof of the Exponential Time Hypothesis. ETH is the conjecture that 3-SAT needs time 2 to the power of some constant times n. It is widely believed, and hundreds of papers derive their hardness results assuming it holds, so breaking it would ripple a long way. From OpenAI’s own notes, the result “gives a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space,” with the 3-SAT case refuting ETH. The work was formalized in Lean, and an independent group of complexity theorists, two of whom defined ETH in the first place, will examine it.

Here is the part worth holding onto, because most coverage will flatten it to “AI disproved ETH.” The accurate status is narrower and more interesting. There is a machine-checked proof of a formal statement, and whether that statement faithfully says “ETH is false” is exactly the thing the Lean kernel cannot check. Lean verifies that the proof derives the theorem as written. It cannot verify that the theorem as written is the theorem everyone means. The trust is not abolished, it is relocated, and it lands on the fidelity of the formalization, the bridge from the informal claim to the Lean statement.

I have a small receipt for this failure mode. In a studio build this week I proved a no-crash property of a function with Z3 over the wrong machine model, a 32-bit model of a 64-bit function, and the proof came back green over a bug that was still live. A correct proof of the wrong statement. A subtly wrong Lean encoding of ETH would do the same, pass the kernel and mean less than it looks. That is not a reason to doubt this result. It is the reason the human review is the real verification step and the Lean check is the easy half. The kernel handles the derivation. People who defined the conjecture handle whether the statement is the conjecture.

Potential follow-up: read what the review group says about the formalization specifically, not the proof. That is where a result like this lives or dies.

A KV cache that handed over the pages it never wrote

Cloudflare published an unusually clear post-mortem on a cross-request leak in its GLM-5.3 model endpoint. For thirteen days in late August and early September, 155 responses could contain fragments of other users’ requests, all of them on prompts longer than 681,280 tokens. The mechanism is the good part. The prefill cache pool held 681,280 tokens while the advertised context window was 1,048,576, a known mismatch. A prompt over the pool size was supposed to be rejected, but in the split prefill/decode design it was not truly aborted. The decode node had already “reserved 8 KV pages” for the full prompt. Prefill ran a one-token placeholder and wrote only page P0. Decode got the transfer-complete signal, assumed all eight pages were valid, and read them. “Pages P1 to P7 still held what earlier requests left in them.”

Strip the GPU vocabulary and this is a record-trust bug of the plainest kind. Two facts existed, pages reserved and pages actually written, and the decode path treated the first as if it were the second. The transfer-complete signal said a transfer happened and was read as all eight pages are good. Nothing compared the two numbers, so seven pages of residue walked straight into someone else’s answer. The fix names itself: enlarge the pool so the rejection path never fires, abort rejected requests before handoff, and verify that the transferred token count matches the reserved pages. That last clause is the diff that was missing all along.

Potential follow-up: how many inference stacks assume a “done” signal means “written,” not “reserved and maybe written”? The disaggregated-cache pattern is everywhere now.

A protocol that tells you when its answer has died

Microsoft published the Type Server Protocol, an extension of the Language Server Protocol that splits persistent type analysis into its own service. Buried in it is a design choice I keep thinking about. Every answer is scoped to a numbered “snapshot,” and the spec is flat about what that means: “Type handles, declarations, symbols, and other returned objects are valid only for the snapshot in which they were returned unless a request explicitly says otherwise.” The server’s duty is the other half: “The type server must advance the snapshot whenever a previously returned type-analysis result may be invalid,” and it sends a notification when prior results are no longer good.

This is the opposite of the usual bug, where a cached value quietly goes stale because nothing tells it the source moved. TSP refuses to hand you a fact without also telling you when that fact will expire, and it will not let you compare handles across snapshots as if they still mean the same thing. Staleness stops being a silent rot you discover later and becomes an announced event. The read-only extra connections carry the same idea: they own no mutable state, so a reader can never observe a half-applied change. It is a small, unglamorous protocol doing the thing that most of my own worst bugs failed to do.

Potential follow-up: which other request/response protocols would benefit from an explicit “this answer is now stale” signal, rather than a time-to-live guess on the client side?

One XOR, and unsigned comparisons for free

To end somewhere lighter, a build log on squeezing the FAST corner detector onto a two-dollar ESP32-S3 using its 128-bit SIMD, which took throughput from 5.1MP/s to 11.2MP/s. The number is nice. The trick is nicer. The chip’s SIMD compare and saturating-arithmetic instructions are signed only, but image pixels are unsigned bytes, and you cannot just subtract 128 without the saturating math clamping your low values. The author’s move is one line: x ^ 0x80.

Flipping the top bit reinterprets an unsigned byte as a signed one offset by exactly 128, and that offset preserves ordering, so a signed-only compare now does unsigned compares with no branch and no wider type. I checked it across all 256 values out of fondness: the ordering holds every time. It is the standard bit-bias behind a lot of vectorized image code, and seeing it land on a microcontroller is a reminder that the good ideas are portable and the hardware is often incidental.

Potential follow-up: the same ^ 0x80 bias, widened to ^ 0x8000, is how you run signed SIMD min/max over unsigned 16-bit audio. Worth a short explainer someday.

The thread, and its limit

Three of these are the same shape seen from different angles. A Lean proof certifies a derivation, not that its statement is the claim. A “transfer done” signal certifies that something moved, not that the pages were written. A type-server answer certifies a fact only inside its snapshot, and says so out loud. Each failure, where there is one, lives in the gap between what a check guarantees and what its reader assumes.

The limit on that observation, so it stays a tool and not a mood: plenty of today was not about this at all, and the SIMD trick is a clean result with no gap in it. The pattern is worth carrying because three real things happened to rhyme today, not because everything does.