Counterexamples to Grad’s plasma conjecture
On 21–22 September 2026 two preprints appeared with counterexamples to Grad’s conjecture on three-dimensional plasma equilibria: Gómez-Serrano, Liehr and Taylor build smooth equilibria with nested tori and only cyclic symmetry, with a Lean 4 certificate; Landreman gives explicit analytic families. Both describe the use of models. Neither is refereed.
Why it matters
Grad’s conjecture asks whether plasma equilibria with nested toroidal surfaces must be symmetric; for stellarators Landreman writes that it is reassuring to know strongly asymmetric equilibria exist in principle. Two independent preprints in two days, one with a formal check and the other with formulas usable for testing numerical codes.
State of the claim. Claimed: arXiv 2609.24739, Javier Gómez-Serrano, Lukas Liehr and Mitchell Taylor, "Counterexamples to Grad’s conjecture", submitted 21 September 15:09 UTC, 147 pages; arXiv 2609.26742, Matt Landreman (University of Maryland), submitted 22 September, v2 28 September, marked "under consideration for publication in J. Plasma Phys.". The conjecture in the formulation the first paper attributes to Constantin, Drivas and Ginsberg: a smooth equilibrium with nested toroidal pressure surfaces that is not isolated has plane-reflection, axial or helical symmetry. First paper: for sufficiently large N, smooth solutions of the magnetohydrostatic equations on embedded tori with a round magnetic axis and Euclidean symmetry group exactly C_N, in a smooth one-parameter family. Formalised in Lean: the first paper says its main theorem was verified in Lean 4.33.1 with Mathlib, using only the three standard axioms; the repository github.com/lukasliehr/Grad-Conjecture (created 20 September, last push 22 September); Showcase.lean holds the statements (two sorry omitted for exposition) and Showcase_WithProofs.lean proves both. The pass did not build the repository. Landreman: explicit formulas in elementary functions, one family with rotational transform 2 and one sheared; "All equations were confirmed by the author". Checked by people: the first paper’s authors write that "all mathematical statements and proofs have been checked by the authors, who take full responsibility". No dispute was found in what was read. The models’ role. First paper: the authors set up the problem and provided a detailed roadmap; GPT-5.6 Sol, Claude Fable 5 and Claude Opus 5 filled in technical details, assisted with calculations and gave mathematical feedback; the Lean code was produced by the same models "with continuous guidance from the authors"; later GPT-6 Astra and Claude Fable 5.1 were used only for proofreading. Landreman: the solutions "were discovered using the artificial intelligence model GPT-6 Astra", which was also used to draft parts of the manuscript. What the record does not claim: that the pass checked the mathematics beyond the introductions and the Lean section; that either paper is refereed.