Chain of Custody
OpenAI announced a resolution of Navier–Stokes, and the week promptly melted down over provenance: the two mathematicians whose year-long private collaboration ran the same route published a statement that became a 2,000-point Hacker News thread, and the durable question — whose sessions train what — got no answer. Meanwhile DeepSeek shipped an MIT-licensed frontier model priced thirty times under Astra, Trail of Bits proved Fermat's Last Theorem with a Lean bug, and the most-installed artefact of the week was a Markdown file asking agents to get to the point.
The tools
i-have-adhd coding open source
A skill for coding agents — Claude Code and the rest — that forces ADHD-friendly output: the answer first, then numbered steps, no 'hope this helps' filler, no burying the fix in paragraph six. MIT-licensed pure instructions, installed by pasting one line into your CLI; the README's before/after examples make the case better than any pitch, and it ships translated into seven languages.
40,000 stars and the top of GitHub trending all week — more than ten thousand of them in the last seven days — plus 535 points on Hacker News. The name is doing real work: it frames agent verbosity as an accessibility problem rather than a taste complaint, and the adoption curve says the frame landed. In a week of trillion-parameter drama, the most-installed artefact in the ecosystem was a Markdown file asking models to get to the point.
tool page →Desert Ant Labs local-ai free tier
A new European lab, launched this week by Paul Veugen, shipping eighteen specialised on-device models for audio, vision, and text: transcription it claims runs 4.7× faster than Whisper, audio enhancement in 9MB, PII redaction across 27 languages in 12MB, language identification in 2MB. Everything runs on the phone's neural engine or in-browser WASM; Swift, Kotlin, and JS SDKs; free up to 100,000 monthly active devices, no tokens, no logins.
484 points on Hacker News for the counter-programming of the week: while everyone argued about half-trillion-parameter models, someone shipped useful ones measured in megabytes. The benchmark numbers are all the lab's own — treat them as claims until someone independent runs them — but the shape of the bet, a fleet of tiny task-specific models instead of one giant generalist, is the interesting part either way.
tool page →YuE2 audio
An open music-generation model from a HKUST-led consortium that works the way musicians do: it first writes an editable symbolic score — ABC notation you can actually change — and then synthesises vocals and accompaniment from it. 3.6B parameters, trained on 346,000 hours of mostly CC0 and synthetic audio, with companion models for audio-to-lead-sheet transcription. The code is Apache 2.0; the weights on Hugging Face are CC-BY-NC — non-commercial, mind.
The score-first architecture is the real news: previous open Suno challengers generated audio you could listen to but not edit, and putting a symbolic plan in the middle makes the output a document instead of a blob. The claim of rivalling Suno v5 is the consortium's own; the editable middle layer doesn't need that claim to be useful.
tool page →Copperhead coding freemium
'Cursor for circuit boards': an agent that designs and verifies PCBs by editing KiCad files directly — schematic, layout, BOM — running electrical and design-rule checks through kicad-cli, keeping the docs in sync, and generating gerbers at the end. `npm i -g copperhead` and bring your own Claude or GPT key; the CLI is Apache 2.0 and free forever, the cloud tier is $49 a month and free for open hardware.
The week's best Show HN at 246 points, and the natural sequel to last issue's EEBench, which measured whether models can design circuits at all — top score 61.6%. Copperhead is the workflow bet that the answer is already yes-enough with a human in the loop, and being graded by ERC, DRC, and eventually a fab gives it the same can't-sweet-talk-the-checker property this newsletter keeps applauding.
tool page →Worth reading
The document behind the week's 2,000-point thread. Buckmaster (NYU Courant) and Levent Alpöge — a mathematician at Anthropic — spent a year in a private two-person collaboration pushing a forced-blowup program at the Millennium Prize problem, working with Claude and Codex, and Lean-verified their breakthrough on August 22. His statement says that after rumors of the unpublished result leaked, OpenAI pointed an internal model and a team down the same route, announced a roughly 100-page resolution days later, would not answer whether the pair's Codex sessions were used in training, and proposed he publish under his name alone, without his Anthropic co-author. He is careful about what he is not claiming — he hasn't seen the proof and accuses no one of copying — which is exactly what makes the document land. Read Willison's companion piece for the durable half: nobody can audit what their sessions train.
Trail of Bits found a soundness bug in Lean 4: for one astronomically large slice position, a string function's logical definition and its compiled native code disagree, and via `native_decide` that disagreement becomes a contradiction — from which you can prove anything, Fermat included, in a few lines. The Lean team shipped the memory-safety fix within ninety minutes. The moral, in the very week AI labs were waving Lean certificates at Millennium Prize problems: machine-checked means your trust moved to the checker, and `native_decide` quietly adds a compiler to that trusted boundary. The same shop also shipped coop this week — a CLI that runs Claude Code and Codex inside disposable Firecracker VMs, which is the fix their own August essay demanded.
The immediately actionable one: Dan Luu had coding agents implement Zstd compression under 26 prompt conditions at roughly eighty runs each — TDD, property-based testing, fuzzing, mutation testing, formal tools — scored against hidden tests with token costs tracked. The finding that should reach your CLAUDE.md: agents use most of these techniques superficially, wrapping ordinary unit tests in specialised frameworks, and plain no-guidance instructions beat most technique-specific prompts. Only a carefully hand-built custom skill outperformed, and imperfectly.
From the big labs
The first model on DeepSeek's Causal Encoder-Decoder architecture: 552B total parameters with asymmetric activation — 8B active on prefill, 16B on decode — a million tokens of context, natively multimodal, and a KV cache squeezed to 890 bytes per token. MIT weights on Hugging Face, and API pricing that reads like a typo: $0.15 per million input on a cache miss, $0.60 out, roughly thirty times under GPT-6 Astra at peak. The benchmark table is vendor-written as usual, pitting it against Opus 5 and GPT-5.6 Sol; Artificial Analysis's early independent read puts it well above the median for its class, and open weights mean nobody has to take anyone's word for long.
Public beta from September 10: build agents that run on OpenAI's infrastructure with the Codex harness handling sessions, orchestration, context compaction, and recovery — you supply the tools and pick the execution environment, with sandboxes managed by OpenAI or self-hosted via Cloudflare, DigitalOcean, or Oracle. No platform fee beyond tokens and tool usage. It is the strongest push yet to move the agent loop itself into the vendor's cloud — which, after this particular week, is exactly the location a lot of engineers have fresh questions about.
Not to be confused with Muse Spark, the model family from last issue — Muse is a consumer app, launched to US users at free, $20, and $100 tiers, that does tasks (shopping, scheduling, forms) inside a 'Muse Secure VM': a dedicated per-user machine with its own browser. Meta says VM data and conversations stay out of the ad systems, a sentence in which the word 'says' is doing an enormous amount of work — 735 largely sceptical Hacker News comments agree. The architecture is the part to note regardless: the per-user disposable computer is becoming the consumer default, not just the security crowd's habit.