Vintage: 2026-09. Primary evidence is Buckmaster’s fetched statement PDF (2026-09-08) plus companion PDF/GitHub links, as synthesized in 2026-09-08-x-morning-buckmaster-alpoge-ai-fluid-proofs-openai-credit. Companion PDFs were not re-parsed page-by-page. Forced smooth blowup ≠ Clay unforced Navier–Stokes.

Buckmaster–Alpöge: Lean-checked forced Euler / Boussinesq / IPM blowups

One-line summary: tristan-buckmaster and levent-alpoge announced Lean-checked finite-time blowup with smooth forcing for incompressible porous media, Boussinesq, and 3D Euler (8 Sep 2026). LLM-assisted (Claude, Codex / GPT-5.6 Sol; Astra writeups/audit only). Not the Clay Millennium unforced Navier–Stokes prize.

The insight

This is a dated verifiable-layer math result: Lean-checked blowups on forced variants. The clip’s grain is “Millennium adjacent / forced variant,” not “Navier–Stokes solved.” Hypo-dissipative NS is claimed internally and not released today (Lean unfinished). Parallel unforced Euler candidate lives on anandkumar-unforced-euler-candidate — do not collapse. Credit-dispute allegations live on openai-fluid-proofs-credit-dispute — do not flatten into this page’s math grain.

It is a mid-2026+ instance of the verifiable-layer spike on ai-math-capability-jaggedness (Lean check). It is not a definition- or conjecture-generator result and does not close can-llms-choose-the-right-research-question. Do not collapse into claude-flt-lean-formalization (known FLT path, different problem).

Evidence

All bullets are from 2026-09-08-x-morning-buckmaster-alpoge-ai-fluid-proofs-openai-credit (method: grok-bot; x_video: false). Permalinks and issuer URLs live on the source page.

Statement PDF — three public results

• From 2026-09-08-x-morning-buckmaster-alpoge-ai-fluid-proofs-openai-credit (statement PDF, fetched 2026-09-08): with levent-alpoge, public today are three results — finite-time blowup with smooth forcing for incompressible porous media, Boussinesq, and 3D incompressible Euler.
• From the same source (same PDF): they believe they also have hypo-dissipative Navier–Stokes blowup but are not releasing that paper today (Lean unfinished; no presentable writeup).
• From the same source (same PDF): credit for the program’s basic idea goes to Diego Córdoba and Luis Martínez-Zoroa (rough forcing → they + LLMs pushed to smooth forcing / Euler). Personal collaboration only — “free of any institutional agreements” with either employer.
• From the same source (same PDF): LLMs used — Anthropic Claude, OpenAI Codex (esp. GPT-5.6 Sol), Astra “only used for writeups and auditing.” Timeline claimed: Aug 15 blowup results for Boussinesq and Euler; Lean verify of a first LLM proof Aug 22.
• From the same source: companion writeups euler.pdf, ipm.pdf, boussinesq.pdf; Lean repo github.com/tristanbuckmaster/fluid_lean. Linked from X; not re-parsed page-by-page in this clip.

X amplifiers (not substitutes for the PDF)

• From the same source (@deaneyang): mirrors Buckmaster’s Mastodon announce with the PDF/GitHub set.
• From the same source (@AndrewCurran_): posts the full statement link set after deleting a prior post.

What this source does not establish

• Not Clay Millennium unforced Navier–Stokes. Forced smooth blowup ≠ unforced NS prize. Discourse that says “Navier–Stokes solved” is wrong.
• Not a rewrite of claude-flt-lean-formalization. Different theorem, different authors, four days later.
• Companion PDFs not page-parsed. Existence + titles only.
• OpenAI’s afternoon forced-NS C/D claim is a different object — file on openai-forced-navier-stokes-claim. Do not collapse this page’s forced Euler into that forced NS. OpenAI’s unforced Euler side-result is openai-unforced-euler.
• Morning OpenAI NS hearsay (Buckmaster’s report of what he was told) stays on openai-fluid-proofs-credit-dispute.
• No person pages for Córdoba / Martínez-Zoroa / Dean Yang / Andrew Curran.
• No ticker.

Contradictions / tensions

• Forced vs unforced vs Clay NS: this page = smooth forced Euler/Boussinesq/IPM; anandkumar-unforced-euler-candidate = unforced Euler candidate on R^3; openai-unforced-euler = OpenAI issuer unforced Euler; openai-forced-navier-stokes-claim = OpenAI forced NS C/D. None of these is Clay unforced A/B. Not collapsed.
• From 2026-09-08-x-afternoon-openai-navier-stokes-images-2-5 (issuer Concurrent work + @OpenAI): OpenAI congratulates forced-Euler priority and says proofs differ (their Euler forced vs OpenAI unforced). OpenAI-side framing — not a rewrite of this page’s Lean objects.
• Released vs withheld NS: hypo-dissipative NS believed internally, Lean unfinished, not public today.

Open questions

• Do independent Lean auditors confirm the fluid_lean statements match the intended PDFs?
• Does the withheld hypo-dissipative NS paper appear, and is it still forced?

Related

• tristan-buckmaster
• levent-alpoge
• anandkumar-unforced-euler-candidate
• openai-forced-navier-stokes-claim
• openai-unforced-euler
• openai-fluid-proofs-credit-dispute
• claude-flt-lean-formalization
• ai-math-capability-jaggedness
• mathematics-in-the-age-of-ai
• math-verification-loop-to-jagged-ai-progress
• automated-ai-research-llm-capability-boundary
• can-llms-choose-the-right-research-question — status stays open; do not close as yes
• anthropic
• openai
• gpt-6-astra
• gpt-5-6-sol-pricing