On Tue, Sep 8, 2026 at 9:43 PM Matt Mahoney <[email protected]> wrote:
> OpenAI today (Sept 8 2026) solved Navier Stokes, one of the seven $1 > million Clay Millineum problems, in 88 hours by a collaboration of 10,000 > agents running an unreleased model. It took another 17 hours on their most > advanced public model to produce a Lean model so that the proof can be > mechanically verified. > As with test harnesses, Lean proofs are subject to phony results that merely assert things even when the accompanying comment text specifies the criteria. This happened to me while preparing a paper for publication in Stuart Kauffman's Festschrift celebrating his 80th birthday <https://github.com/jabowery/RelativeIdentity>. Fortunately, I caught it before the deadline. ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/Tf866419d43752e9c-Me9fcc1214d0d5f0318713f5d Delivery options: https://agi.topicbox.com/groups/agi/subscription
