A public preprint presents counterexamples to Grad’s conjecture with a Lean formalization. This is a mathematical statement about magnetohydrostatic equilibria, not a demonstration of an operating fusion reactor. Readers should inspect the exact hypotheses and the proved companion artifact before converting a formal-verification headline into a broader scientific or engineering conclusion.
What the paper claims
The September 21 preprint by Javier Gómez-Serrano, Lukas Liehr and Mitchell A. Taylor constructs families of smooth magnetohydrostatic equilibria on embedded solid tori. Its claim concerns configurations with a finite cyclic symmetry group rather than the symmetries contemplated by Grad’s conjecture. The paper also describes a Lean 4 certification. We report the authors’ mathematical claim without asserting a FyreLinkz proof audit, plasma experiment or independent confirmation of every argument.
Choose the proved companion, not only the showcase
The repository distinguishes Showcase.lean, which has two presentation placeholders, from Showcase_WithProofs.lean, its proved companion. A Comparator checks their statement correspondence and dependencies. It pins Lean 4.33.1 and describes separate builds. Those distinctions are important: a presentation artifact with placeholders is not the same thing as the claimed proved dependency chain. We have not run those builds. The linked repository is the identified source, not permission to assume every similarly named plasma project establishes the same theorem.
Read the theorem before the significance
Our suggested reading starts by listing the domain, smoothness conditions, pressure structure, boundary conditions and definition of symmetry. Ask which assumptions a proposed counterexample satisfies and which stronger statements it does not address. If a popular summary removes a hypothesis, flag that sentence for review. A useful explainer should make a specialist’s disagreement precise: is it about the encoded theorem, its correspondence to the paper or the interpretation of the conjecture? A model’s confident explanation is not a substitute for that distinction.
Formal equilibrium is not device performance
For engineering readers, our recommendation is to keep existence results and experimental performance in separate columns. A mathematical configuration does not by itself provide hardware tolerances, operating stability, manufacturing constraints or net-energy measurements. We do not predict a reactor launch date or an electricity cost from this preprint. Before linking the theorem to a design decision, ask a relevant expert which additional physical conditions must be established. That conversation can be valuable without pretending the paper answers questions it never set out to resolve.
A reproducible verification note
If you reproduce the formal build, record the commit, toolchain and exact target, then retain the complete output. Explain which statement was checked and how you examined its correspondence to the informal claim. Do not describe a successful download or a presentation-only build as independent proof validation. We would update this article with a qualified audit or a meaningful correction. The OpenAI math reading guide explains the same separation between research claims, formal artifacts and revision status in a different release.
Frequently asked questions
Did this demonstrate an operating fusion reactor?
No. It concerns mathematical equilibria and a formalization, not a reactor experiment.
Are the two showcase files equivalent evidence?
The repository distinguishes the placeholder presentation from the proved companion and supplies correspondence checks.
Did FyreLinkz compile the formalization?
No. We reviewed the paper and repository documentation without running the builds.
Sources & further reading
Primary sources checked Oct 11, 2026. Vendor statements are attributed; editorial advice is our own.
- 1Counterexamples to Grad’s conjecture ↗Javier Gómez-Serrano, Lukas Liehr and Mitchell A. Taylor / arXiv
- 2Grad-Conjecture formalization and companion distinctions ↗Lukas Liehr and collaborators
Help us keep this useful. Check contact availability →
