Skip to main content
Watch: Grok Bot Built My AI Video Arena While I Tested 8 Models

Briefing · Sunday, August 2, 2026

Cursor Hides the Dollars, Seedance 2.5, and a Lean Kernel Bug

Cursor Hides the Dollars, Seedance 2.5, and a Lean Kernel Bug

Good morning. It's Sunday, August 2, and we're covering Cursor's quiet switch from dollars to tokens, ByteDance's Seedance 2.5 video model, a soundness bug in Lean's kernel exposed by an AI-assisted proof attempt, and Kimi K3 running faster on AMD hardware than on Blackwell.

Two things happened this week that cut against the developer-tool trust budget at once: Cursor removed dollar figures from its usage page for individual plans with no announcement and no opt-out, and an AI-assisted "disproof" of the Collatz conjecture slipped through Lean's kernel only to be caught days later. Both are worth understanding in detail.

In today's brief:

  • Cursor replaced dollar amounts with token counts on the usage page; enterprise plans keep dollars, individual plans do not, and there is no setting to switch back
  • Seedance 2.5 generates 30-second audio-video clips in one pass, with up to 30 images, 10 video clips, and 10 audio clips as references
  • An AI-generated "proof" of False exploited two unrelated kernel bugs in Lean; the postmortem from Leonardo de Moura explains the fix that landed one hour after the report
  • Wafer serves Kimi K3 on AMD MI355X at 952 tok/s per node and says it beats the B300 on performance per dollar

THE BIG ONE

Cursor Made the Usage Page Token-Only, and It Was Deliberate

The Cursor forum thread that started late on July 31 (325 points, 148 comments on HN) reads like a small revolt: users who watched the Usage window daily for spend tracking opened it and found dollar amounts replaced by token counts, with no changelog entry and no setting to change it back. "I use this Usage window closely to keep tabs on my daily/active spending," the original post reads. "Today, the $$ amount is replaced by token amount which is completely useless."

Cursor staff confirmed the change is intentional. "There isn't currently a setting to switch back to dollar amounts for individual plans," a staff reply reads. "Enterprise Plans will still show dollar amounts here, but individual plans will not." The reasoning given: individual plans include generous included usage, so displayed dollar amounts were "often higher than the user's plan cost," which confused people. On the token-based Ultra plan, covered usage now shows token counts marked "Included," and only on-demand spend beyond the plan shows a dollar figure in the Cost column. Dollar totals still exist in two places: Dashboard > Spending shows an On-Demand Spending figure for the current cycle, and the CSV export's Cost column carries dollar amounts per on-demand row.

The community's response zeroed in on what the move hides. "Cursor needs to be transparent about the per-request cost if that is what we are being billed for," one reply reads. "This is unacceptable and makes it impossible for team members to track their own personal usage when working on a team with a shared on-demand usage cap." Our full analysis of the change covers what still shows dollars, what the CSV contains, and how to reconstruct your own spend.

Why it matters: When the tool that bills you decides you no longer get to see the bill in your money, the missing number becomes the product decision - and every usage-based tool that follows this path raises the same trust question.

MODELS

Seedance 2.5: 30-Second Clips in One Take, With 30 Reference Images

ByteDance's Seed team launched Seedance 2.5 on July 31 (344 points, 185 comments on HN), and the release leans hard on a single idea: a generation should be a complete creative work, not a clip. The model produces up to 30 seconds of audio-video in a single pass and supports multi-round extension with improved shot transitions and scene changes, so multi-minute pieces keep a consistent audiovisual language. Referencing is the other headline - a single pass can take up to 30 images, 10 video clips, and 10 audio clips as inputs, plus clay render, motion, and creative references, which is aimed squarely at characters that need to stay recognizable across scenes.

Editing got the professional push: timestamp-level control for targeted audio-video edits, plus green screen, camera-perspective, and reference-based editing. The HN discussion split between awe at the coherence ("Their washing machine advert example seems like it's as good as anything else on social media," one commenter wrote) and skepticism about who pays for it ("Are these video models' only actual use case misinformation and spam?"). The counterpoint came quickly: major brands are already running AI-generated spots, and one commenter pointed out that reference-based generation is what makes usable ad work possible - a face, product, or set that stays right across 20 cuts. No open weights were announced, and the top comment got the thread's bluntest summary: "No weights, no care."

Why it matters: Thirty-second coherent generations with multi-round extension move video models from one-shot demos to editing tools - and referencing turns a model into a studio that can keep a brand consistent.

RESEARCH

An AI-Assisted Collatz "Disproof" Found a Real Bug in Lean's Kernel

The most quietly significant story of the week is Leonardo de Moura's postmortem of Kernel Soundness Bug #14576 (150 points on HN). On July 25, Ramana Kumar published a sorry-free "disproof" of the Collatz conjecture produced with AI assistance. It was not a valid proof: it exploited a bug in Lean's kernel handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and filed issue #14576. The fix merged one hour after the report.

The bug: when the kernel eliminates a nested occurrence under an inductive type whose parameters are phantom (not mentioned in constructor fields), those parameters disappear from the generated auxiliary type and escape type checking - so an ill-typed argument could be used to make the kernel accept a proof of False. It is reachable only through metaprogramming, and it is an implementation bug, not a hole in the meta-theory. The uncomfortable part is that there were two unrelated bugs involved: the official kernel missed a check in nested inductive support, while nanoda, the independent Rust kernel by Chris Bailey, checked that spot but missed a type name in a projection node. The proof was built so the expression the kernel never inspects is one the old nanoda accepted. Mario Carneiro's lean4lean verification is affected too, since its handling of inductives is a port of the reference implementation.

The postmortem's practical conclusions: independent-kernel checking still works - it took two distinct bugs in two implementations to slip through - but users need current versions of both. And de Moura pushes back on the instinct to restrict metaprogramming: the elaborator is untrusted by design, and a malicious proof can be submitted as a compiled .olean file or through memory modification, so only the kernel rejecting ill-typed declarations on its own counts. Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity; it found other programming mistakes in the kernel, all now fixed, all caught by nanoda.

Why it matters: A frontier model found a soundness bug in the most-verified proof assistant in existence - and the defense that held was exactly the one formal methods promises: independent checkers, current versions, and a kernel that trusts no one.

LOCAL INFERENCE

Kimi K3 on AMD MI355X: Faster Per Dollar Than a B300 Node

Wafer published benchmarks of Kimi K3 served on AMD MI355X (129 points, 39 comments on HN) that make a strong AMD case. Kimi K3 is 2.78 trillion parameters - over 1.5 TB of VRAM before a KV cache - which is too big for a B200 node and requires either B300s (288 GB per GPU) or two B200 nodes in TP16. The MI355X also has 288 GB of VRAM per GPU, at roughly 2.4x cheaper per GPU than a B300 and 1.7x cheaper than a B200. On a 1,024-token input / 400-token output benchmark, an 8x MI355X node hit 952 tok/s aggregate and 118 tok/s single-stream - 3.8x the aggregate throughput per node of the TP16 B200 deployment (498 tok/s across 16 GPUs) and 1.3x the single-stream decode.

The B300 still wins on raw throughput, about 1.65x aggregate per node, but at 2.4x the price. Wafer's verdict: the MI355X "crushes the B300 on performance per dollar," helped by AMD shipping day-0 support for Kimi K3, which removed most of the integration work that usually punishes AMD in inference. The caveat is honest: AMD software support has been the reason frontier serving on non-NVIDIA silicon is an engineering project, and Wafer's claim is that agents are now good enough at kernel and model optimization to close that gap. Our Kimi K3 developer guide covers the model itself, and the wafer results are worth reading for the per-token economics.

Why it matters: If AMD stays within 1.6x on throughput while costing 2.4x less, the open-weights frontier gets a second hardware ecosystem - and GPU-vendor lock-in stops being the default assumption for frontier serving.

PLATFORMS

Stateless MCP Recaptured Simon Willison, and We Agree

Tuesday's rollout of the 2026-07-28 Model Context Protocol specification - the "MCP 2.0" that drops sessions entirely - got its most useful writeup from Simon Willison, who built three tools against it in one week: an mcp-explorer, a datasette-mcp plugin, and an llm-mcp-client integration. His argument for coming back around to MCP after preferring agent skills through 2025: giving an agent a shell with internet access is fraught, while MCP tools are easier to audit and control, and simple enough that smaller laptop-runnable models can still drive them.

The spec change is genuinely simplifying. Legacy MCP needed two HTTP requests - an initialize handshake that returned a Mcp-Session-Id, then the actual tool call. The new stateless transport makes every request one self-contained POST, no session to hold, no server state to route back to, which is what unlocks serverless and horizontal scaling for MCP servers. We covered the wire-level changes and a Bun pattern for hosting a fleet of MCP servers on one process, and the Vercel MCP migration clock if you are adopting the new spec.

Why it matters: The most significant MCP change since launch makes servers trivially deployable and auditable - which is exactly what a tool that hands an agent your API surface needs to be.

PLATFORMS

NetBSD 11.0 Ships With an Honest List of Open Security Issues

NetBSD released 11.0 on August 1 (286 points on HN), the first major release in years, and its release note contains a rarity: an explicit statement that the release ships with known, listed open security issues because the flood of AI-assisted vulnerability reports makes a zero-open-issues release impossible. "The number of security issues found or suspected everywhere has massively increased with the advent of AI tools," the note reads. "As a consequence, we can't publish a release without open issues. Instead of delaying the release further to fix them, we've instead chosen to be transparent about this."

The listed items are concrete: hdaudio(4) needs access checks on ioctl commands (with an easy manual workaround - remove /dev/hdaudio*), ipfilter has a remotely triggerable null pointer dereference but is not in any released kernel by default, and pf has a use-after-free in fragment reassembly and is deprecated. The release was also delayed by waiting for third-party components to make stable releases so fixes could land. It is a useful counterpoint to the polished "all clear" release notes most projects publish, and a reminder that the AI-vulnerability wave the Lean kernel bug illustrates is being felt in every corner of systems software.

Why it matters: A major OS release admitting its open issues, by name and with workarounds, is the transparency pattern the AI-vulnerability era is going to force on everyone - better to copy NetBSD's approach than to ship silent debt.

TOOLS WORTH A LOOK

  1. Go 1.27 Interactive Tour (free) - VictoriaMetrics took over Anton Zhiyanov's interactive tour series (218 points on HN) with runnable examples of the release's headline feature: generic methods, which let a method declare its own type parameters independent of the receiver.
  2. mcp-explorer and datasette-mcp (free / OSS) - Simon Willison's stateless MCP tools, built in a day each against the new spec; a uvx-runnable MCP explorer and a Datasette plugin.
  3. NetBSD 11.0 (free / OSS) - the long-awaited release with split ISO images, U-Boot images for ARM, and the most honest security notes in OS release history.

WHAT ELSE IS HAPPENING

Every link above goes to a primary source or our sourced coverage. Tomorrow's brief lands when the news does - subscribe to get it by email.

Get the next one in your inbox

The daily brief, delivered. Free, unsubscribe anytime.