From magnetic geometry to a design proof.
A rigorous, staged plan for turning stellarator models, numerical candidates, and engineering data into explicit Lean-checked contracts.
Why stellarators? Why formal proofs?
Explore the original illustrated introduction: magnetic confinement, the torus and its field lines, the role of AI discovery, and the architecture of a verified design library.
Explore the illustrated overview →One design, several proof obligations.
No single “stable” flag is enough. A practical claim composes equilibrium, stability, particle confinement, transport, component, and uncertainty contracts around the same candidate.
Physical laws, empirical fits, validity ranges, boundaries, norms, and horizons remain visible in every claim.
External solvers propose candidates. Exact decoders and proved checkers establish only the claims their soundness theorems support.
Progress is reported by reviewable artifacts, from an honest kernel through a robust integrated candidate.
Detailed workstreams
Each chapter preserves the complete planning note and gives every tracked task an explicit progress field.
Library method
How PlasmaLean separates domain assumptions, sanity checks, and verified theory.
0 tracked tasks01 · FoundationModel contracts
What a design proof can claim, how contracts compose, and where assumptions live.
5 tracked tasks02 · PhysicsGeometry & fields
Pressure surfaces, flux coordinates, field-line dynamics, quasisymmetry, and near-axis theory.
10 tracked tasks03 · PhysicsModels & equilibrium
Ideal MHD, static and weak equilibria, boundary conditions, and model reductions.
9 tracked tasks04 · PhysicsMHD stability
Energy principles, continuum operators, neutral modes, and honest stability certificates.
10 tracked tasks05 · PhysicsParticles & transport
Full and reduced orbits, confinement horizons, kinetic transport, and reactor profiles.
10 tracked tasks06 · VerificationVerified numerics
Exact inputs, continuous bounds, equilibrium validation, and certificate identity.
9 tracked tasks07 · DesignCoils & design
Biot–Savart fields, inverse coil design, manufacturing geometry, and robust workflows.
9 tracked tasks08 · DesignVacuum demonstrator
Checked tolerance-aware calibration fixture, the CNT reference direction, and the remaining boundary to a practical stellarator.
5 tracked tasks09 · DesignMaterials & engineering
Heat, stress, magnets, quench, neutronics, lifetime, power, and maintenance.
10 tracked tasks10 · ProgramRoadmap
Evidence gates, the first coding sequence, research questions, and progress records.
26 tracked tasks11 · ProgramLiterature
Primary sources, extraction discipline, software roles, and theorem reading order.
9 tracked tasksThe first coding sequence
The initial sequence builds reusable, auditable results before attempting a full three-dimensional candidate.
Definitions, tangency, and witnesses
Conservation, coercivity, and zero modes
Exact decoding and checker soundness
Continuous curve and clearance bounds
Exact thermal margin over an input box
Source-distance and derivative bounds