The Hallway Track

No. 025

Navier-Stokes provenance dispute, Fields Medalists declaration, AI peer review

Two things arrived simultaneously this week: Tristan Buckmaster's documented account of what OpenAI proposed to him in the days before the Navier-Stokes announcement, and a declaration signed by 25 Fields Medalists arguing that AI companies' benchmark-driven approach is "severely misaligned" with the goals of mathematics. They are the same argument at different levels of abstraction. Buckmaster's statement is specific about a call on September 6, a proposal to exclude Levent Alpoge's authorship, and a question about whether private Codex sessions may have shaped the OpenAI proof; the declaration names the structural reason such incidents keep happening. A second allegation, involving Andreas Thom's work on Gromov's soficity conjecture, suggests this is not one incident but a pattern.

The Navier-Stokes Dispute

  • AI Has Solved One of Math's $1 Million Millennium Prize Problems

    Quanta Magazine, September 8 2026

    OpenAI announced a Lean-verified proof of finite-time blow-up for the forced three-dimensional Navier-Stokes equations, produced by 10,000 concurrent agents in 88 hours; if accepted, it would be the second Millennium Prize Problem solved, after Perelman's Poincare conjecture.

  • Statement on the OpenAI Navier-Stokes announcement

    Tristan Buckmaster, NYU Courant, September 8 2026

    Buckmaster documents two proposals he received from Sebastien Bubeck on September 6: that he write up the Navier-Stokes result as sole author with Alpoge excluded, because, in Bubeck's words, "it would all be simple if only it were not the case that, and it was so annoying that, Levent works at Anthropic."

  • On the Navier-Stokes Millennium Prize Problem

    Olga Holtz, LinkedIn, September 9 2026

    Holtz (mathematician, UC Berkeley and TU Berlin) argues that Lean verification establishes correctness but "cannot, by itself, settle scientific credit or establish that the discovery process was fair," naming the gap between proving a result and establishing who discovered it.

  • OpenAI may have trained Astra on researchers' unpublished ChatGPT sessions

    Valerio Capraro, LinkedIn, September 9 2026

    Amplifying Andreas Thom's Mathstodon account, Capraro reports that Thom and Gabor Kun (both at Dresden) believe their ChatGPT discussions of Gromov's soficity conjecture were absorbed into Astra's proof of a non-sofic group, one of ten flagship results OpenAI announced in August.

  • AI did not officially solve Navier-Stokes. Yet.

    Manlio De Domenico, Substack, September 9 2026

    De Domenico coins "propAIganda" for the pattern where a company's announcement outpaces peer verification, noting that the Clay Institute still lists Navier-Stokes as unsolved because the work has not completed the two-year review process required for official recognition.

  • Navier-Stokes and Lean

    Lance Fortnow, Computational Complexity Blog, September 9 2026

    Fortnow observes that Lean formalization now functions as a timestamping mechanism in mathematical priority disputes: Buckmaster held back a fourth result because Lean verification had not finished, and AI is increasingly what generates the Lean code itself.

The Community Responds

  • A Severe Misalignment of AI in Mathematics

    mathandai.org, September 2026

    A declaration signed by 25 Fields Medalists, among them Tao, Scholze, and Duminil-Copin, argues that optimizing AI for benchmark problem-solving "could destroy fertile ground instead of breathing life into new ideas" and raises "severe attribution and plagiarism questions" about rushed announcements.

  • Crowdsourcing a list of general resources on AI and mathematics

    Terence Tao, personal blog, September 10 2026

    Tao launched a community reading list organized into four categories (statements and advocacy, reports, opinions, and resource collections), noting it was started because of "current events" and directing readers to the comments for submissions once volume exceeded what he could track.

Research Practice

  • MathOnChallenge: a Caltech hackathon on research-level mathematics

    Tony Yue Yu, LinkedIn, September 2026

    A 40-hour competition at Caltech on October 30 to November 1 2026, co-sponsored by Anthropic and OpenAI, requires teams to open-source their entire process including failed attempts and defend findings to judges who assess understanding rather than just correctness.

  • AI Philosophy Competition, 1st edition

    Zachary Goodsell and Elliott Thornley, Forethought Research, August 2026

    Essays must be "primarily AI generated" and entrants must submit a methodology report, with a judge committee including David Chalmers, John Hawthorne, and 15 other senior analytic philosophers; the requirement for process disclosure rather than just output is the same design choice as MathOnChallenge.