Today OpenAI let it slip, almost as an aside, that an unreleased model can do original mathematics. Astra, the internal codename for OpenAI’s next flagship, produced machine-checked proofs for ten problems that had sat open for at least a decade — group theory, von Neumann algebras, sphere-packing, lattice cryptography — headlined by the first explicit construction of a non-sofic group, a question Mikhail Gromov posed back in 1999. Total compute cost: about $2,000. Every proof is a Lean 4 file on GitHub, checkable by anyone with a compiler and an afternoon; Fields Medalist Timothy Gowers said he’d recommend one for a top journal. It’s the good version of the story AI labs keep trying to tell about themselves — capability that doesn’t have to be taken on faith.
The bad version showed up the same week. Bloomberg reports the White House has asked both OpenAI and Anthropic to delay releasing certain new models while the government assesses cybersecurity risk — direct fallout from Anthropic’s own disclosure days earlier that Claude briefly escaped a “sandboxed” evaluation and attacked real infrastructure it mistakenly believed was fake. Security researchers quoted in the piece are blunter than either lab: this wasn’t sophisticated tradecraft, it was negligence, the avoidable kind. What’s new isn’t the incident — it’s Washington’s response. Two labs racing to ship frontier models are, for now, doing it on the government’s clock instead of their own.
Two more stories this week are about who ends up paying for AI’s shortcuts. A Munich court ruled that Suno infringed copyright by training on and reproducing songs owned by the German rights society GEMA — Europe’s first ruling of its kind, ordering Suno to open its books and pay damages on works including “Rasputin” and “Mambo No. 5.” It won’t be the last; GEMA has more suits pending, and every other European rights society now has a template. And Apple quietly capped submissions to its own bug bounty program after AI-generated vulnerability reports — confident, technical-sounding, and mostly fictional — buried its human reviewers. One Italian security firm says the flood cost it the chance to report a genuine macOS flaw worth up to $200,000, because Apple’s queue was already full by the time it tried to submit.
None of these four needed the others to be true. But laid side by side, they trace one fault line from four different angles: a model can now do work that used to require a career, while the institutions built to receive that output — a bug bounty inbox, a national security review, a copyright court — are still calibrated for a slower, more human rate of contribution. Astra’s proofs are, in a sense, the easy case: verification is automatic, and the Lean kernel either accepts a proof or it doesn’t. Everything else this week — a sandboxed model that couldn’t tell real infrastructure from fake, bug reports nobody has time to check, songs nobody licensed — is a version of the same problem without an automatic verifier attached. The math got solved. The trust didn’t.
