← Back to PlasmaLean Exposition Hub
AI & Lean 4 Stellarator Engine

PlasmaLean: Designing a Practical Stellarator with Machine-Checked Mathematics

Bridging Small-Kernel Formal Verification, Differential & Complex Geometry, and 3D Fusion Engineering

Portal: siddhartha-gadgil.github.io/PlasmaLean/

Core Philosophy: Isolate physical model contracts into a tiny, human-auditable Lean 4 kernel backed by non-vacuity sanity checks—enabling AI agents and mathematicians to collaborate with zero specification drift.

The Core Physics Problem

Why Stellarators Are a Pure Geometry Optimization Problem

Tokamaks (2D Axisymmetric)

  • Continuous rotational symmetry $\partial_\phi \mathbf{B} = 0$.
  • Noether's theorem automatically conserves canonical toroidal momentum $P_\phi$, confining particle orbits.
  • Fatal flaw: Requires megiamperes of inductive plasma current $\implies$ violent disruptions & pulsed operation.

Stellarators (3D Non-Axisymmetric)

  • External 3D twisted modular coils create rotational transform $\iota(\psi)$ without driven plasma current.
  • Challenge: Breaking 2D symmetry destroys $P_\phi$ unless the 3D field satisfies Quasisymmetry: $|B(\psi, heta,\phi)| = B(\psi, M heta - N\phi)$.
Pillar 3 · Architectural Trust

The Small-Kernel & Sanity-Check Pattern

Why do numerical stellarator optimizers hit "false optima", and how do formalizations avoid proving vacuous theorems?

1. Small Trusted Kernel (~120 LOC)

  • Defines $ abla \cdot \mathbf{B}$, $ abla imes \mathbf{B}$, regular flux surfaces $\psi^{-1}(c)$, and coil-to-plasma clearance $d_{\min} > 0$.
  • Zero project-specific axioms (only standard Lean 4 propext, Classical.choice, Quot.sound).

2. Non-Vacuity Sanity Checks

  • Proves $\mathbf{B} \equiv 0$ is rejected by HasFluxSurface.
  • Proves $d_{\min} > 0$ prevents Lean's real division trap x / 0 = 0 in Biot–Savart integrals.
  • Constructs analytical circular torus witnesses satisfying the full contract.
Pillar 4 · Compiled Milestone

Anatomy of a Tolerance-Aware Vacuum-Fixture Certificate

Compiled Today in PlasmaLean: From smooth 3D coil curves $\gamma_i : S^1 o \mathbb{R}^3$ to certified manufacturing margins:

  1. Clearance Enclosure: Certify $\inf_{s, x \in \Sigma} \|x - \gamma_i(s)\| \ge d_{\min} > 0$.
  2. Exact Biot–Savart Fréchet Derivatives: Machine-checked Jacobians $\partial_y K(x,y, au)$ and $\partial_ au K(x,y, au)$.
  3. Banach Lipschitz Perturbation Bound: For all coil warps $\|\delta\gamma_i\|_{C^1} \le arepsilon < d_{\min}/2$, bound $\|\mathbf{B}(\gamma+\delta\gamma) - \mathbf{B}(\gamma)\| \le L_{ ext{BS}}(d_{\min})\, arepsilon$.
  4. Toroidal Surface Atlas Certificate: Guarantee $|\mathbf{B}\cdot\mathbf{n}|/\|\mathbf{B}\| \le \eta_{\max}$ across all of $\Sigma_{ ext{target}}$.
Pillar 1 · Rosetta Stone

Translating Physics into Pure Geometry

Stellarator Physics Differential / Complex / Symplectic Geometry
Flux surface $\psi = c$ Compact regular level set $\Sigma_c \cong T^2$ of a first integral ($\mathcal{L}_B \psi = 0$)
Vacuum field ($ abla\cdot B=0, abla imes B=0$) Harmonic 1-form $eta \in \mathcal{H}^1(M, g)$ ($deta = 0, d^*eta = 0$)
Force-free field ($ abla imes B = \lambda B$) Beltrami 1-form $\star deta = \lambda eta$ (Contact structure $eta \wedge deta eq 0$ when $\lambda eq 0$)
Rotational transform $\iota(\psi)$ Poincaré rotation number of area-preserving poloidal return map
Guiding-center particle drift Hamiltonian flow of Littlejohn's non-canonical symplectic 2-form $\Omega_{GC}$
Non-folding Fourier surfaces ($\sqrt{g} > 0$) Univalence of planar harmonic maps on $\mathbb{D} \subset \mathbb{C}$ (Radó–Kneser–Choquet)
Invitation #1 · Topology & Dynamical Systems

Open Targets for Topologists

1. Arnold–Poincaré–Hopf Toroidal Foliation

From $\mathbf{J} imes \mathbf{B} = abla p eq 0$, prove $(\mathbf{B}, \mathbf{J})$ trivializes $T\Sigma_c$, forcing $\chi(\Sigma_c) = 0$ and $\Sigma_c \cong T^2$.

Stub: Challenge1_PoincareHopfTorus.lean

2. Gauss Linking & Converse KAM

Formalize homotopy invariance of the Gauss linking integral $\mathrm{Lk}(\gamma_1, \gamma_2)$ for modular coils, and MacKay's Converse KAM criteria to bound magnetic island chaos.

Stub: Challenge2_GaussLinking.lean

Invitation #2 · Differential & Symplectic Geometry

Open Targets for Differential Geometers

3. Parallel Bishop Frames & Tubular Reach

Frenet frames fail when curvature $\kappa(s)=0$ (quasi-isodynamic stellarators). Formalize parallel Bishop frames $(T, N_1, N_2)$ and prove the tubular neighborhood Jacobian $\det(D\Phi) = 1 - r_1 k_1 - r_2 k_2 > 0$ for $r < 1/\kappa_{\max}$.

Stub: Challenge3_BishopFrameNearAxis.lean

4. Littlejohn Symplectic Form & Noether

Prove that $(M,N)$-quasisymmetry $\mathcal{L}_u |B| = 0$ generates an exact conserved helical momentum $P_{ ext{hel}}$ under guiding-center symplectic dynamics.

Stub: Challenge4_QuasisymmetryNoether.lean

Invitation #3 · Complex Geometry & Harmonic Analysis

Open Targets for Complex Geometers

5. Univalence of Harmonic Fourier Maps

Certify that double Fourier series $(R_{m,n}, Z_{m,n})$ define non-overlapping flux surfaces ($\det D\Phi > 0$) using complex-analytic $\ell^1$ contraction and Nehari/Radó–Kneser–Choquet univalence criteria on $\mathbb{D} \subset \mathbb{C}$.

Stub: Challenge5_HarmonicUnivalence.lean

6. Riemann Surface Modulus $ au(\psi) \in \mathbb{H}$

Every flux surface $\Sigma_\psi \cong \mathbb{C}/(\mathbb{Z} + au(\psi)\mathbb{Z})$ carries a Hodge star $\star_g^2 = -I_2$ and period matrix determined by its conformal modulus $ au(\psi)$.

Stub: Challenge6_ConformalTorusModulus.lean

Get Involved

How to Contribute in 15 Minutes

  1. Browse the Rosetta Stone & 10-Min Kernel Audit to see the exact Lean 4 types.
  2. Pick a Self-Contained Lean 4 Bounty Stub from lean_stubs/Challenge1..6.lean (each file imports only Mathlib—no physics solver setup needed!).
  3. Replace sorry with a Lean 4 Proof (using human insight, grind, or AI theorem-proving assistants) and open a PR to siddhartha-gadgil/PlasmaLean.