DHH compares AI coding agents to the effect of the Kodak Brownie on portrait painting and says 37signals is done writing code by hand. The next version of Hey drops the web app for six native clients built by agents and a Rust backend. He keeps Rails for web apps, where convention over configuration helps token efficiency. He urges apps to ship CLIs for agents and argues for optimism over doom.
Quentin Adam, head of the French cloud provider Clever Cloud (about 70 developers), argues that coding agents have changed the developer’s job: what matters now is the specs, architecture and tests, not the code itself. He wraps AI output in unit, integration and simulation tests, runs automated pentests on every commit, prefers Rust for its strict compiler, and aims to retire all legacy code in 2026. Companies that skip this harness, he says, see little gain.
Chung, Du and Wesley study “the Station,” an open-world environment with no central coordinator. Agents from different model families choose research directions, run experiments and publish papers that later agents read and cite. On 12 construction problems from the AlphaEvolve study, five gave results new to the literature, including a new infinite family of finite field Kakeya sets and an improved lower bound for Erdős’s minimum overlap problem. The results rest on exact constructions or Lean-verified proofs.
An unreleased research version of Claude, asked to “take a real stab” at the Riemann hypothesis, did not prove it. It did raise the known lower bound for the proportion of zeta zeros on the critical line from 41.6% to 67.2%, building on work by Aryan, Baluyot et al., and Bombieri. Two Anthropic mathematicians validated the paper, and a Lean formalization passes the standard comparator check.
OpenAI presents ten results on long-standing open problems, each described as resolving or making substantial progress on one. They were produced by an internal version of its next model, Astra. Topics include sphere packing, binary codes, permanent lower bounds, quantum parallel repetition, closest-vector hardness, a disproof of Connes’s rigidity conjecture, and Erdős problems 146, 180 and 183. Humans prepared the manuscripts with the model, which formalized each argument in Lean.
Bessis argues that mathematics’ honor code, which rewards proven theorems and treats concept-building and exposition as secondary, leaves the field exposed to AI. Machines may win at problem-solving and be credited with “solving math” while producing unintelligible proofs that add nothing to understanding. He cites First Proof and Math Inc’s 200,000-line Lean formalization of Viazovska’s sphere-packing work, and urges mathematicians to say publicly that the product of mathematics is understanding, not theorems.
Ronacher describes using Pi to build Pi and argues that LLM-rewritten issues and PRs, full of confident but wrong diagnoses, now create extra work for maintainers. He asks reporters to state only what they observed. In the last 90 days, only 60 of 714 auto-closed external PRs, about 8%, were eventually merged. He also criticizes agents for adding local workarounds instead of keeping global invariants, such as those of Pi’s session log.
Jonas Templestein builds an agent harness where everything, including streaming LLM chunks and errors, is an event in an append-only stream with its own URL. Each feature is a stream processor: a reducer derives state from events, and a hook performs side effects such as LLM calls. The log makes runs easy to debug, and plugins can run elsewhere, in any language, or be deployed by appending their code as an event.
]
