OpenAI model solves Navier-Stokes equations: Anthropic formalizes proof for Fermat’s Last Theorem

In today’s edition of Data Points, you’ll learn about our top headlines, and more:

• Muse, Meta’s agentic personal assistant
• AlphaGenome Atlas, a database of DNA effects
• ChatGPT Images 2.5, a better image editor
• Voice Design, an easier route to multi-regional agents

But first:

OpenAI model proves major unsolved mathematical result

OpenAI said an internal AI system produced a proof showing that the Navier-Stokes equations, which model fluid motion and have stood unresolved since the 1930s, can develop a singularity in finite time, resolving one of the Clay Mathematics Institute’s seven Millennium Prize Problems. The work used an unreleased model described as more capable than GPT-6 Astra, running roughly 10,000 concurrent coordinating agents that could read a cached internet snapshot and execute code, reaching the solution 88 hours after launch on September 5, with formalization in Lean (a proof-verification language) taking another 17 hours. Along the way, a smaller group of under 100 agents disproved a related question, the unforced Euler equations’ regularity problem, in about 50 hours. Across the full effort the agents exchanged 4.9 million messages and generated roughly 300 billion output tokens; OpenAI says it is not claiming the $1 million Clay Prize itself and is instead using the result to demonstrate model progress. OpenAI also disclosed it reached out to Anthropic researcher Levent Alpöge and NYU professor Tristan Buckmaster after hearing rumors they had solved a related forced Euler problem, and is crediting their independent work in a joint announcement. Importantly, OpenAI said it could not rule out that its unreleased model had not been trained on Buckmaster and Alpöge’s work. (OpenAI)

Anthropic model proves even bigger (but already solved) mathematical result

Anthropic said an internal research model built on Claude produced the first complete, computer-checked formalization of Fermat’s Last Theorem in Lean, a proof assistant that verifies mathematical logic step by step. Multiple Claude agents worked largely autonomously over 11 days, writing 13 million lines of Lean code and proving 30,300 intermediate propositions, 29,500 of which made it into the final proof. The agents coordinated through Prove2Me, an open platform that tracked which propositions still needed proving so parallel agents didn’t duplicate work or lose track of progress. The proof adapts a simplified exposition of Andrew Wiles’s 1995 proof, uses Lean’s three standard axioms, and was checked against Mathlib’s own statement of the theorem; the effort used about six billion output tokens. Mathematician Kevin Buzzard, who led a separate multi-year formalization project at Imperial College London, reviewed the proof and called it an autoformalization achievement built on solid prior work. Formalization here means machine-checking an existing proof’s logic, not discovering new mathematics, but the speed of this result points toward AI eventually helping catch errors in published math and easing the burden of reviewing AI-generated proofs. (Anthropic)

Meta releases Muse Spark-based shopping and planning agent

Meta introduced Muse, a personal AI agent that can plan and execute multi-step tasks like book travel, negotiate deals, or handle a dinner party menu, accessible through the Muse app or WhatsApp. It runs on Muse Spark, Meta’s newest model, inside a dedicated cloud virtual machine called Muse Secure VM. The VM pairs Muse with a separate “Sentinel” agent that must approve any outbound internet action and asks the user for permission when needed. Muse stores connected credentials in secure storage it can use but not see, checks in before sending emails or making purchases, and pays using a Stripe-built Link wallet that issues one-time-use cards and covers eligible purchases with return and price-drop protections; Shop Pay and 1Password support are coming soon. Meta says people can disconnect services, tell Muse to forget specific memories, and opt out of having their interactions used for AI training, and it plans an encrypted “Confidential VM” version later this year that even Meta cannot access. Muse is rolling out in the US on iOS, Android, and the web, free for basic use with paid plans for heavier usage. The launch gives developers a look at Meta’s approach to giving an agent real purchasing power while trying to firewall it from sensitive data. (Meta)

Google unveils giant human DNA prediction database

Google DeepMind released AlphaGenome Atlas, a database of precomputed predictions for the molecular effects of all 9 billion possible single-letter DNA variants in the human genome. The dataset is 1 petabyte in size, more than 30 times larger than the AlphaFold Database, and is built by running the AlphaGenome model at scale across the genome. It ships with a new AlphaGenome Variant Impact (AVI) score that combines AlphaGenome with AlphaMissense to rank both coding and non-coding variants by likely impact, plus a catalogue of over 2,500 recurring DNA sequence motifs. The Atlas is free for academic use via a web portal, the AlphaGenome API, and as a skill in Google Antigravity, with commercial access coming later on Google Cloud. External collaborators have already used the Atlas to identify a disease-causing DNM1 variant and to uncover 22 percent more non-coding genetic associations in UK Biobank data. This gives researchers a precomputed shortcut to variant-impact predictions instead of running AlphaGenome themselves for every query, though DeepMind stresses it is not validated for clinical use. (Google)

OpenAI’s updated image model doesn’t degrade between edits

OpenAI released ChatGPT Images 2.5, a new image generation and editing model rolling out today to all ChatGPT, ChatGPT Work, and Codex users on desktop, mobile, and web. The model cuts generation latency by up to 50 percent compared with Images 2.0, better preserves subjects from reference photos across edits, and handles multi-turn editing instructions without degrading quality over time. New ChatGPT features include Sketch, which turns a hand-drawn reference into a finished image, plus image comments, prompt sharing, and templates for formats like posters and product photos. Developers get two API models: GPT-Image-2.5 Flare, the default option offering higher quality than GPT-Image-2 at 50 percent lower latency, and GPT-Image-2.5 Sunburst, aimed at premium workflows needing tighter edit control but with longer generation times. The consistency improvements across edits give developers a more reliable way to make targeted changes to an existing asset — like swapping a product or background — without rebuilding it from scratch. (OpenAI)

Gradium generates new synthetic voices from prompts

Gradium, a Paris-based voice AI company spun out of the Kyutai research lab, launched Voice Design, a feature that turns a written description into one to five new synthetic voices in three to five seconds, with no reference audio or speaker rights needed. The feature is free on every Gradium plan, in both the API and Studio, and accepts descriptions of up to 500 characters in English, French, Spanish, Portuguese, or German covering traits like accent, pitch, pace, and register. Unsaved candidates expire after 30 days and are limited to REST calls with 100-character audition text; converting a candidate to a full voice is free and gives it normal access to streaming TTS, WebSocket, and Speech-to-Speech endpoints, using one of 5 custom voice slots on the free tier or 1,000 on paid plans. Gradium’s own blind listening test across 7,627 comparisons in five languages reported a 72.6 percent win rate against five rival systems, including ElevenLabs at 59.0 percent, with the largest margins on regional accents like Quebecois French (97 percent); these figures are vendor-run and not independently verified. For developers building voice agents, this removes the sourcing and licensing overhead of cloning when a catalog lacks the specific accent or character a project needs. (MarkTechPost)

Want to know more about what matters in AI right now?

Read the latest issue of The Batch for in-depth analysis of news and research.

Last week, Andrew Ng discussed how use of coding agents is evolving, emphasized a high-level workflow for software development from planning to execution and deployment, and concluded with the importance of directing workflows, enabling agent autonomy, and customizing agent environments.

“I find that social media often gives oversimplified descriptions of how to use coding agents. For example, it is sometimes useful to get agents to run autonomously for hours and burn millions or tens of millions of tokens. But currently the practical utility of very long-horizon tasks — especially relative to their cost — has been amplified beyond reality. Instead, most effective coding agent use is a complex, highly iterative process, and being able to intervene with high-skill judgement gives much better results.”

Read Andrew’s letter here.

Other top AI news and research covered in depth:

• Comparing OpenAI and Anthropic’s Data Retention Policies highlights how OpenAI’s Private Safety Processing and Anthropic’s Enterprise Frontier Safeguards impact Zero Data Retention (ZDR) policies.
• Ox Alpha Revealed as GLM-5.3-Flash showcases Z.ai’s latest model that gained viral attention as Ox Alpha, utilizing China-made chips for its deployment.
• Custom Models for Law, News, and Finance explores Thomson Reuters’ Thomson LLM, which is based on Qwen 3.5 and trained on proprietary data to enhance domain-specific applications.
• A Simpler Method to Monitor Models introduces CRC Monitor, a tool capable of detecting incorrect or unsafe model output in real-time, improving AI safety and reliability.

A special offer for our community

DeepLearning.AI’s first-ever subscription plan for our entire course catalog includes foundational classics like the Machine Learning and Deep Learning specializations plus seminars on the latest tools and frameworks you need.

As a Pro Member, you’ll immediately enjoy access to:

• Nearly 200 short and long AI courses from Andrew Ng and industry experts
• Labs and quizzes to test your knowledge
• Projects to share with employers
• Certificates to testify to your new skills
• A community to help you advance at the speed of AI

Enroll now to lock in a year of full access for $25 per month paid upfront, or opt for month-to-month payments at just $30 per month. Both payment options begin with a one-week free trial.

Explore Pro’s benefits and start building today!

Try Pro Now!