Paper of the Week #6 — The Check Passed. What Did It Check?
This week: a Lean proof that does not match the paper it formalizes, a decision-model table whose test sets are in its training mix, labels that override definitions, memory that wins or loses depending on how much the model reads, NCCL symmetric memory gains that depend on payload size and GPU, a 40-49% token cut that needs lowercase and thinking off, and an AI prescribing pilot whose first phase has two physicians check every prescription.
Paper of the Week #6 — The Check Passed. What Did It Check?
Oct 5 – 9, 2026 · Lean and Navier–Stokes · Unsloth decision models · labels vs definitions · agent memory · Dust · EmbeddingGemma 2 · NCCL symmetric memory · cablese · Utah AI prescribing · Erdős Problems
Ten items this week, and most of them share a question: a check passed, but what did it actually check? A Lean proof compiles but proves a slightly different lemma. A test set is "decontaminated" but its dataset is in the training mix. A prescription is "AI-issued" but, in the pilot's first stage, two physicians approve it first. For each item: what came out, the numbers we checked in the source, what to watch for, and whether you can check it yourself. Four of them we measured ourselves this week, and those link to the full posts.
Lean compiled. Does it prove the paper's lemma?
What came out. "Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs" (Alexander Bastounis, King's College London; Fabian Circelli and Anders C. Hansen, University of Cambridge; arXiv 2610.08144, 6 October) examines the Lean code OpenAI released alongside its natural-language proof of finite-time blowup for Navier–Stokes. The abstract says "the formalised Lean proof does not correspond to the NL proof."
The part worth reading. Example 3.1. Lemma 8.6 of OpenAI's paper bounds an operator using four more derivatives of the input (m + 4); the corresponding Lean theorems all use five (m + 5), which is a strictly weaker statement. We checked the Lean repository at the commit the paper cites: norm_derivativeWord_inverse_le in NavierStokes/SmoothFamilyTorusInverse.lean assumes bounds on w.length + 5 derivatives, and the declaration is unchanged on main. The paper finds a second mismatch in a pressure-flux bound.
Watch for. The authors say plainly: "We do not make claims about the correctness of OpenAI's NL proof, we only make statements about mistranslations into Lean." So "the proof is wrong" is not what this paper shows; "a passing Lean check does not certify the natural-language argument" is. We found no response from OpenAI or the formalizers yet (the repository has two commits, both before the paper, and issues are disabled). All four figures in the paper are screenshots of conversations with ChatGPT-6, and in Figures 3 and 4 the chatbot agrees with the authors on the two Navier–Stokes mismatches. That is weaker evidence than the code comparison itself.
Check it yourself. Partly. Comparing equation (8.19) with line 1063 of that Lean file takes ten minutes; judging whether m + 5 breaks the downstream argument takes a PDE specialist.
"Decontaminated," and still the same dataset
What came out. Unsloth published a guide to training your own Jev-style decision model (docs; the training code was merged on 7 October). Its table, measured by Unsloth, has Qwen3.5-0.8B going from 7% to 74% on BANKING77 and from 19% to 76% on CLINC150 in about 4 GB, and says the test sets were "decontaminated against the training data."
What we found. We trained it ourselves with Unsloth's own script and defaults, three seeds per condition, decision rule fixed before training. BANKING77 and CLINC150 matched the table (75.4% and 75.0%). Both datasets are in the training mix, though, and "decontaminated" means dropping training rows that share 13 consecutive words with a test row; for these short messages that removed 3 rows from BANKING77 and none from CLINC150. With the two datasets taken out of training, the same 500 test rows scored 56.5% and 55.9%, about 19 points lower. typed-decisions came out at 61.2% against the table's 73%, and the same 13-word check turned out to drop 850 of its 1,200 training cases. In a post hoc run that kept them in training, typed-decisions reached 74.3%, within 1.3 points of the table.
Watch for. Nothing in the guide is false; it reports in-domain accuracy. If your task is intent classification over intents that weren't in training, 56% is the closer guide.
Check it yourself. Yes, on one GPU: peak memory was 4.15 GB, and each run took about 20 minutes on our GPU, which was shared with another job. Our full write-up: we trained our own decision model.
Labels override definitions
What came out. "Labels Override Definitions in Jev-Style Typed Decision Models" (Azizi, Baghaei Potraghloo, Pedram; arXiv 2610.02586) asks whether open decision models follow the option definitions you write or the option names. Deleting every definition leaves laya-td's accuracy unchanged (0.8559 vs 0.8487). The cause it points to is one line of prompt rendering, not the weights: rendering definitions only makes all three laya checkpoints exactly invariant to the labels.
Watch for. The paper's +0.1511 from renaming options to A and B comes from a synthetic suite built so the rule lives only in the definitions. On the paper's eleven classification tasks, laya-td's definitions alone, with labels replaced by letters, reach 0.7971, below 0.8559 with labels and definitions together. Hosted Jev was not measured.
Check it yourself. Yes. We reran it on two of the paper's three laya checkpoints (laya 0.3.7): the one-line patch reproduced the exact invariance on both, and labels that contradict their definitions dropped TREC accuracy from 88.6% to 22.2%. Full post: our rerun.
Agent memory: the answer depends on how much the model reads
What came out. Two papers that look like they disagree. "When Does Selection Replace Extraction?" (Rishabh Sharma and Rishika Lall, independent researchers; arXiv 2609.34227, pre-registered, code MIT) compares storing raw conversation turns and picking the relevant ones with Jev against memory systems that extract facts when writing. On 778 held-out LoCoMo questions with gpt-4o-mini answering, raw turns picked by Jev scored 77.0% against 77.5% for the authors' own extraction system, non-inferior by its pre-registered margin (lower bound −3.0 against −5), at 3,061 times lower write cost. VibeMemBench (arXiv 2609.23570, SIAT, SUAT and Alibaba) finds that 11 of 12 pairings of coding agent and memory system fail to beat the same agent with memory off.
The part worth reading. The budget. In the first paper, reranking 30 candidates helps a lot when the answer model reads 3 items (+17.4 points on LoCoMo, +9.1 on LongMemEval) and barely at 20 (+1.5 and +1.1), where extraction systems are more accurate. The same paper reports that reranking lowers correct abstention: at 3 items, adversarial questions answered by abstaining fell from 63.6% to 54.1%. "Is memory worth it" has no answer without "how many items does the model read."
Watch for. VibeMemBench kept only targets where injected history improved the outcome in a reference setting, as its abstract states, so its set is built to give memory a chance; 11 of 12 failing on that set is the stronger for it, but it is not a sample of all coding tasks. In the first paper the blind human regrade was done by the first author, on the 141 questions where the single judge model (gpt-4o-mini) marked one system right and the other wrong.
Check it yourself. The first paper's make reproduce-v3 rebuilds every number from committed result files with no API calls. Rerunning the experiments needs paid OpenAI and Jev calls.
Dust: pretraining without backprop
What came out. Q Labs' Dust (Dahal, Mandal, Gülbahar, Vegesna; paper, code MIT) trains a transformer language model with no backward pass, perturbing activations and turning loss changes into updates. It reports ending below backprop at 1M tokens from about a thousand draws per update, and says it does not try to be compute-efficient enough to replace backprop.
What we found. At 1M tokens with the authors' code, Dust at 1,024 draws reached 5.938 against 5.941 for SGD backprop over 20 seeds; any gap is under about 0.02, and the paper's 0.025 did not appear. Backprop with the paper's own Adam settings reached 5.384 in the same single epoch, and backprop with the paper's SGD recipe reached 5.209 after 16 passes over the same data, at 4.6% of Dust's compute. Full post: Dust rerun.
Watch for. Dust at 1,024 draws spends about 347 times backprop's compute per step. The interesting claims are at 10M and 20M tokens, which we did not run.
EmbeddingGemma 2 and Korean search
What came out. Google DeepMind released EmbeddingGemma 2, a 740M open embedding model (Apache 2.0) with a 270M text core. Its card reports multilingual MTEB 61.36 against 61.15 for the first generation, and no Korean on its own.
What we found. On our own 177 Korean/English post pairs, with each post's description as the query, the first generation ranked the right Korean post first more often: 162 against 153 (p = 0.022), and 164 against 155 when the target was the English post (p = 0.035). English to English showed no difference. Full post: EmbeddingGemma 2 in Korean.
Watch for. Descriptions share words with their posts, which makes these queries easier than real questions; BM25 tied EmbeddingGemma 2 on Korean to Korean.
NCCL symmetric memory: up to 2.5 times on small all-reduces, slightly slower at 8 GiB on B200
What came out. Stas Bekman added NCCL symmetric memory measurements to ml-engineering on 5 October: all-reduce bus bandwidth with and without symmetric buffers on an 8×B200 node and an 8×H200 node (torch 2.14.0+cu130, NCCL 2.30.7, mean of two sweeps). On B200, symmetric memory is faster by 154% at 32 KiB, 83% at 1 MiB, 76% at 64 MiB and 12% at 1 GiB, and 2% slower at 8 GiB and 16 GiB. On H200 the gain shrinks from 133% at 32 KiB to 3% at 1 GiB and never turns into a loss.
Watch for. It requires every rank to be reachable over direct NVLink and buffers allocated from a memory pool registered as symmetric (register_mem_pool(pool, symm=True), torch 2.9 or later); a workload that all-reduces ordinary tensors gets none of this. The gains also assume calls queue up while the GPU is busy. Timed with host overhead, waiting on each call, the 32 KiB gain is 37% on B200 rather than 154%. Bus bandwidth is not training speed.
Check it yourself. Only with NVLink. Our A100 PCIe cards are not, so we can't.
Cablese: 40-49% fewer tokens, with two conditions
What came out. "The Telegraph Test" by Travis (GitHub Travis42) (repo, Apache-2.0, data CC BY 4.0) asks a model to write a record of a passage in cablese, the clipped style of 19th-century telegrams, and has other models answer questions from that record. With the instruction to write in lowercase and thinking off, billed output tokens fell 48.4% for GLM-5.3-Flash, 48.9% for Qwen3.8-27B and 40.4% for Gemma 4 31B, over 50 passages. Readers answered at 1.01 to 1.09 times the accuracy they got from plain records, on 727 questions.
Watch for. Both conditions matter. Without the lowercase line the records come out in capitals and the savings are 25-34%. For GPT-5-mini, cablese triggered about three times more reasoning and the write cost doubled. Grading is deterministic code; the author deleted every number an earlier LLM judge had produced after finding the models graded their own answers generously. The setting is records read by other models, not chat answers, and one passage bank.
Check it yourself. Yes. verify_headlines.py recomputes the README numbers from the frozen runs without any API calls; we ran it and got 31 of 31 checks passing. Rerunning the probes on a local Qwen is the next step and costs nothing but GPU time.
"Without direct human oversight," with two physicians in phase one
What came out. Utah's Office of Artificial Intelligence Policy approved a pilot in which Nolla Health's AI issues initial prescriptions, not just refills, for mild-to-moderate acne in Utah adults, from a short list of topical treatments (oral drugs and isotretinoin excluded, per SiliconANGLE). Some headlines said the AI prescribes "without direct human oversight."
Watch for. In Nolla's own description, stage one covers the first 100 patients and runs at least four weeks, and in it "two licensed physicians independently review and approve every AI-generated prescription before it reaches the patient." Moving to stage two, where physicians review after the fact, requires "95% agreement with physicians and zero serious adverse events, and written approval from the state." Some coverage kept the 100 patients and dropped the other two conditions, describing the move as automatic once there are no serious problems. We could not open the state's agreement itself (the site returned 403), so stage details come from Nolla and Healthcare Dive. A separate Utah pilot from January, Doctronic, covers renewals only.
Check it yourself. No, and we make no medical judgment here. The reading lesson is the one that applies: conditions on stages tend to fall out of a headline first.
Erdős Problems freezes proof claims
What came out. Thomas Bloom, who runs erdosproblems.com, announced on 6 October four changes: a "hiatus" on new problem comments and proof claims, no more open or solved statuses, no credit-giving language for future results, "human or AI," and an emphasis on high-quality expositions of proofs. His reason: "the vast majority of the comments the site receives now are people announcing AI-generated proofs," often without explanation, "as a way to record a (increasingly meaningless) priority claim." He calls the changes "somewhat experimental"; existing comments stay as an archive.
Watch for. Bloom also writes that "we now know the answer to many questions we did not before," and that much recent progress came from renewed human effort. In the replies, Sam Korsky said the last two changes (credit language and expositions) seemed fine and objected to the first two (the hiatus and hiding statuses), saying their "only effect" is to make mathematical progress less visible. Statuses are hidden, not reset; solved problems do not become open.
Check it yourself. Nothing to measure; the announcement and its replies are short and worth reading in full.
The Ledger
Issue #5 moved its open items into measurement posts: Suffix Cache Reuse, Clef-flash on our BANKING77 and CLINC150 messages, and an MSMF re-measurement on an A100 PCIe. None ran this week; the GPUs were on the GPT-2 series and the four measurement posts above. The A100s free up after 9 October, and MSMF is the first in line, since it needs half an hour on one card. The older items, the DeepSeek-V2-Lite control and token forcing for the MoE result and HoH at ten iterations, are still open.