AI and maths, Bun in Rust, Claude Opus 4.8

In short: in a few weeks AI has closed a mathematical conjecture open since 1968, rewritten from scratch a JavaScript runtime of a million lines, and received a new flagship model designed to orchestrate hundreds of agents in parallel. The thread running through the three stories isn't the power of the models: it's verification. Each result counts because someone, or something, was able to check it line by line.

The 3 stories in 30 seconds

One prompt, sixty years of waiting. Liam Price, 23, with no advanced training in mathematics, fed Erdős problem #1196 to GPT-5.4 Pro. Eighty minutes later he had a proof, later formalised in Lean and taken up in a paper with Terence Tao among the authors.
Bun has been rewritten in Rust by AI. The JavaScript runtime that is an alternative to Node went from Zig to Rust in an agent-led migration: about 750,000 lines of Rust, eleven days from first commit to merge, test suite passing. It's now available in the canary channel.
Anthropic has released Claude Opus 4.8. Just 41 days after Opus 4.7, with a new feature in Claude Code, dynamic workflows, which lets a single task be spread across hundreds of subagents in parallel.

1. A sixty-year-old problem, no degrees, one prompt

On 13 April 2026 Liam Price, 23, with no advanced academic training in mathematics, did something he does fairly casually: he took one of the Erdős problems, conjectures left open by the mathematician Paul Erdős, and pasted it into GPT-5.4 Pro. One prompt, no additional context.

The problem was #1196, a conjecture by Erdős, Sárközy and Szemerédi on primitive sets: sets of integers in which no element divides another. The question was whether, for sets made up only of large numbers, a certain sum stayed below 1. The best previous result, by Jared Duker Lichtman in 2023, stopped at about 1.399: a 40% margin that nobody could close.

The model reasoned for about eighty minutes and produced a proof, which Price posted on the erdosproblems.com forum. From there the chain started: another user realised it was something serious, and it landed on the desks of professional mathematicians.

Why it's different from the other "AI solves maths" stories

News about AI and Erdős problems has been going round for months, and experts warn that these problems are an imperfect benchmark: they vary enormously in difficulty and importance, and many AI-produced solutions have turned out to be less original than they seemed. This case is different for two reasons.

The first is the method. The decisive move wasn't a new technique but an unprecedented pairing: Markov chains with weights based on the von Mangoldt function, an approach that seems to have escaped the earlier literature ever since Erdős's seminal work of 1935. Things that already existed, applied where nobody had ever put them. The method then proved useful across a whole family of problems, allowing #1217 to be proved as well and a short proof of the Erdős Primitive Set Conjecture (#164) to be given.

The second is verification. The proof was formalised in Lean, the proof assistant that forces you to justify every single logical step: if there is a gap in the reasoning, Lean rejects the proof. There's no room for hedging. Today the problem's official page credits the solution to GPT-5.4 Pro (prompted by Price) and points to the paper signed by Alexeev, Barreto, Li, Lichtman, Price, Shah, Tang and Tao.

And here is the point few people make. An LLM is non-deterministic: same prompt, different answers. It generates plausible outputs, not guaranteed ones. Tao himself has warned about the risk of survivor bias: thousands of attempts are launched at these problems, but practically only the successful ones get reported. The breakthrough isn't that AI solves hard problems. It's that there is now an infrastructure to know when it's right.

2. Bun has been completely rewritten in Rust by AI

Second story, same pattern: enormous output, verification as the deciding factor.

Bun is a high-performance JavaScript runtime, an alternative to Node.js, which came into Anthropic's orbit in late 2025. It was written in Zig. It no longer is.

On 14 May 2026 PR #30412, titled "Rewrite Bun in Rust", was merged into the main branch of oven-sh/bun: 6,755 commits, 2,188 files changed, over a million lines added, starting from a branch called claude/phase-a-port. The branch name says it all about who wrote the code.

The migration in numbers: about 750,000 lines of Rust, 99.8% of the existing test suite passing, eleven days from first commit to merge. Hundreds of agents worked in parallel, with two reviewers assigned to each file.

What it is, and what it isn't

Sumner was explicit in the PR: the rewrite passes the existing test suite on all platforms, fixes several memory leaks and flaky tests, the binary shrinks by 3-8 MB and benchmarks range from neutral to faster. The architecture stays the same, the data structures the same, no async Rust. The main motivation, for Sumner, isn't performance but memory safety: having a compiler that catches a class of bugs that has cost the team years of debugging.

So it isn't a redesign: it's a faithful port at very large scale, the kind of work where repetitiveness rewards agents and correctness can be measured with tests. And verification wasn't only automatic: the PR shows the review traces of different bots (one AI generating, another AI checking) while regressions outside the scope of the benchmarks, platform-specific behaviour and long-term maintainability remain to be assessed with human eyes.

For now the Rust build is available only in the canary channel, pending the remaining optimisation and clean-up PRs: run bun upgrade --canary to try it. It is due to reach the stable channel with version 1.4.0.

3. Claude Opus 4.8 and dynamic workflows

Third story, and it closes the circle: the Bun migration is the use case Anthropic brought as proof of its new tool.

Anthropic released Claude Opus 4.8 on 28 May 2026, just 41 days after Opus 4.7. The model id is claude-opus-4-8, the price is unchanged from 4.7, and it's available on all paid plans as well as the API, Amazon Bedrock, Google Vertex AI and Microsoft Foundry.

Benchmarks improve almost across the board, but the most interesting figure is another: Opus 4.8 is about 4 times less likely than 4.7 to let a flaw in the code it wrote slip through without flagging it, and is more willing to state its own uncertainties. For work that runs unsupervised, this matters more than any score.

Dynamic workflows: hundreds of agents on a single task

The feature that changes things operationally is in Claude Code. Dynamic workflows let Claude plan a job and then execute it by spreading it across dozens or hundreds of parallel subagents in a single session, with verification built into the process, so that results are checked before they reach the user. The cap is 1,000 subagents.

Two warnings, given by Anthropic itself. The first: dynamic workflows consume far more tokens than a typical session, and the recommendation is to start from narrow tasks to calibrate consumption before launching them on a whole codebase. The second: they're discouraged where deterministic behaviour is needed. On the controls side, the feature is on by default on Max, Team and API, while on Enterprise it's off and must be enabled by an administrator.

The announcement also mentioned Mythos-class models, the tier above Opus: Anthropic stated that Mythos-class models still require additional safeguards before a wider rollout. In early June Claude Fable 5 and Claude Mythos 5 arrived, with access suspended a few days later to comply with US Department of Commerce export controls: a sign of how much cybersecurity capability has become the real regulatory bottleneck of this generation of models.

The common thread: generating is easy, verifying is everything

Three different stories, one operational lesson.

A mathematical proof run through Lean. A million lines of Rust validated by a test suite and cross reviewers. A model designed to say when it isn't sure. In all three cases the value isn't in the AI's output: it's in the system that lets you trust that output.

Using AI well doesn't mean using it a lot. It means building the perimeter within which its work can be checked: tests, typing, formal verification, adversarial review, explicit acceptance criteria. Those who already have that perimeter multiply. Those who don't accumulate technical debt at an unprecedented speed.

Frequently asked questions

Who solved Erdős problem #1196? The proof was produced by GPT-5.4 Pro, prompted by Liam Price, 23, with no advanced training in mathematics, on 13 April 2026. The official page on erdosproblems.com credits the solution to the model, naming Price as the author of the prompt. The result was then taken up in a paper with eight authors, including Terence Tao.

How long did the AI take to solve it? About eighty minutes of reasoning, starting from a single prompt.

How do you verify a proof produced by an LLM? With a proof assistant such as Lean, which checks every logical step automatically and rejects the proof if it finds an unjustified jump, and with review by human mathematicians. In the case of #1196 both routes were used.

Is Bun already in Rust in the stable release? No. The rewrite was merged into the main branch on 14 May 2026 and can be tried via the canary channel (bun upgrade --canary). It is expected in the stable channel with 1.4.0, after the optimisation and clean-up PRs.

Why rewrite Bun from Zig to Rust? The stated reason, from Jarred Sumner, is memory safety: having compiler-assisted tools to prevent a class of bugs that had cost the team a lot of debugging time. The binary is also 3-8 MB smaller and benchmarks come out neutral or better.

What are Claude Code's dynamic workflows? A feature that lets Claude plan a complex task and spread it across dozens or hundreds of parallel subagents (up to 1,000) in a single session, with built-in verification. They consume many more tokens than a normal session.

Does Claude Opus 4.8 cost more than Opus 4.7? No, the base price is unchanged. Fast mode is also quicker and, on 4.8, noticeably cheaper than in previous versions.

Do these stories mean AI can replace mathematicians and developers? None of the three cases suggests so. In all three, the result became usable only thanks to a layer of verification (formal, automatic or human) built around the model's output. The work shifts from production to designing the checks.