On 4 September Anthropic published what it calls the first complete computer-checked proof of Fermat's Last Theorem (FLT). Claude agents, working largely on their own for about 11 days on Prove2Me, wrote roughly 13 million lines of Lean and proved about 29,500 intermediate theorems. Kevin Buzzard of Imperial College London reviewed the artifact and said the autoformalization was robust enough to build on. A comparator confirmed the statement matches Mathlib's own FLT statement, and Lean checked the finished proof against Lean's three standard axioms.

Flag the claims carefully. This is a formalization of the Wiles / Taylor argument (via Darmon, Diamond, and Taylor), not a new mathematical proof of FLT. Anthropic says the run burned about six billion output tokens on an internal research model roughly comparable to Claude Fable 5.1. Mathlib acceptance of the artifact as a library contribution is not claimed. (Anthropic; GitHub)

GitHub said GPT-6 Astra is generally available in GitHub Copilot as of 4 September. That puts the new model into the enterprise Copilot picker for orgs that enable it, alongside the API and cloud paths OpenAI already opened for Daybreak and paying ChatGPT tiers.

This is Copilot policy and admin enablement, not a replay of Thursday's Critical cyber bar. If your developers ask for Astra in the IDE, the question is who turned it on and under which data controls. (GitHub)

Japan Times and Straits Times, citing Reuters, report Washington and Beijing are preparing a mid-September AI safety dialogue, with Treasury's Scott Bessent in the frame and a Trump-Xi meeting on the calendar for 24 September. The agenda talk is cyber risk and how labs police themselves.

A White House official has said no mid-September AI meeting is planned. Treat the dialogue as contested reporting until both sides confirm a date and a room. (Japan Times)

Microsoft Security Research says ASCII smuggling, the invisible Unicode tag trick popularized in AI prompt-injection work, is now showing up in high-volume phishing. Attackers split lure words like "funding" with characters humans do not see, so signature and machine-learning filters miss the string. Defender for Office 365 hunting signatures spiked hard starting 9 February 2026 and stayed elevated for months.

If your mail stack or an agent pipeline ingests raw Unicode, strip or normalize the tag block before you trust a classifier. This started as an AI hunt and landed in ordinary email. (Microsoft)

TechCrunch, citing The Information, says Thinking Machines Lab is in talks to raise about $1 billion at a valuation of at least $40 billion, with existing backer Accel discussing the lead and Nvidia also in the conversation. The lab's seed was a $2 billion round at roughly $12 billion. Revenue run-rate talk sits over $100 million from unnamed sources.

Nothing is closed. "In talks" is not a wire. Multiple and headcount claims stay unverified until Thinking Machines or Accel confirm. (TechCrunch)

Adobe named Anil Chakravarthy chief executive, effective 1 December 2026, with Shantanu Narayen moving to executive chairman. Chakravarthy has been running Digital Experience. The board is betting the next chapter on someone who already sells the enterprise stack.

This is succession in an AI product cycle, not a model launch. Watch whether Digital Experience and Firefly stay one P&L story. (Adobe)

The FLT story is as much about Prove2Me as about Claude. Anthropic says early agent runs failed when workers lost project state. The open collaborative DAG kept theorem statements searchable, parallel, and linked, and that is when the campaign finished. A small follow-on with three Claude Max plans formalized Vinogradov's Three Primes Theorem in three days on the same scaffold.

If your shop is throwing agents at long verification jobs, ask who owns the graph of work, not only which model sits at the leaf. (Anthropic)

The Move

Claude did not invent a new proof of Fermat. It machine-checked an old one at agent scale.

This week, ask your risk and engineering leads one question: when an AI hands us a proof, a patch, or an audit finding, do we have a machine-check path, or only a human queue that cannot keep up?

Write the answer next to the model names on your approved list. Do not leave it as "we trust the vendor."

Seven bullets. One move.