Lean 4 Physics Proof Library
Machine-checked proofs of Maxwell's equations, MHD equilibrium, plasma confinement, and incompressible Navier-Stokes in Lean 4 with Mathlib. 135 definitions and theorems, zero sorry.
What This Project Does
Physics textbooks derive Maxwell's equations, wave equations, MHD equilibria, and the Navier-Stokes equations with informal arguments that skip steps and rely on unstated assumptions. This project formalizes these derivations in Lean 4, forcing every hypothesis to be stated and every logical step to be verified by the compiler.
The result is a library of 135 machine-checked definitions and theorems covering vector calculus on
R3, electromagnetic wave propagation, plasma confinement physics, and
incompressible fluid dynamics. Every proof compiles with zero sorry (Lean's escape hatch for
unfinished proofs), meaning the Lean type checker has verified the logical correctness of each derivation.
Module Overview
Vector Calculus Foundation
All differential operators are defined from Mathlib's Fréchet derivative fderiv,
giving rigorous meaning to gradient, divergence, curl, and Laplacian on R3.
- Partial derivatives via
fderiv R f x (Pi.single i 1) - Curl defined by explicit Levi-Civita pattern matching on Fin 3
- Curl-curl identity: ∇ × (∇ × F) = ∇(∇ · F) − ∇2F
- Symmetry of mixed partials (Clairaut/Schwarz theorem)
Electromagnetic Waves
Starting from Maxwell's equations with linear media parameters (ε, μ, σ), derives the general wave equation and specializes to vacuum, dielectric, and conductor cases.
- Full Maxwell system with free current and charge sources
- General wave equation for E and B fields
- Vacuum wave speed c = 1/√(μ0ε0)
- Conductor wave equation with damping term
Plasma Physics & MHD
The largest module covers ideal and resistive MHD, equilibrium theory, the Grad-Shafranov equation for tokamak-like configurations, and field-reversed configuration (FRC) equilibria.
- Ideal MHD: frozen-in flux, Ampère's law, ∇ · B preservation
- MHD equilibrium: B · ∇p = 0 and J · ∇p = 0
- Grad-Shafranov equation with Solov'ev linear solution
- FRC: β at separatrix, total pressure conservation
- Resistive MHD with Ohm's law and magnetic diffusion
Incompressible Navier-Stokes
Derives the incompressible Navier-Stokes equations and their key consequences including the vorticity transport equation and pressure Poisson equation.
- Full momentum and continuity equations
- Euler equations as inviscid (μ = 0) specialization
- Vorticity transport with vortex stretching term
- Pressure Poisson equation from divergence-free constraint
Technical Approach
Why Lean 4?
Lean 4 is an interactive theorem prover with a large mathematical library (Mathlib) covering real analysis, topology, and linear algebra. The dependent type system ensures that if a proof compiles, it is logically correct — there is no room for hand-waving.
Mathlib provides the Fréchet derivative, smooth function spaces (ContDiff), and continuous linear maps that serve as the foundation for all vector calculus in this project.
Proof Strategies
- Component-wise expansion: Vector identities proved by expanding into Fin 3 components and using
ring/omega - fderiv linearity: Distributing
fderivover +, −, scalar * using Mathlib's differentiation API - Mixed partial symmetry: Connecting
IsSymmSndFDerivAtto component-level commutativity - Structure bundling: Physics systems as Lean structures with positivity hypotheses baked in
Interactive Blueprint
The project includes a LeanBlueprint — an interactive dependency graph that shows how every definition and theorem connects. Each node links to the Lean source code, and the graph gives an immediate visual overview of the entire formalization.
Repository Structure
MaxwellWave/
- VectorCalculus.lean
- Maxwell.lean
- WaveEquation.lean
- ProofSketch.lean
PlasmaEquations/
- SingleFluidMHD.lean
- MHDEquilibrium.lean
- GradShafranov.lean
- ResistiveMHD.lean
- RotamakFRC.lean
- + 5 more files
NavierStokes/
- Equations.lean
- Euler.lean
- Vorticity.lean
- PressurePoisson.lean