• End-to-end formally verified solvers for the electrostatic Vlasov equation (collisionless Boltzmann equation for the one-particle distribution function in phase space, coupled to a fixed electrostatic potential), in 1x1v, 1x2v, 1x3v, 2x2v, 2x3v, and 3x3v (i.e. from 2D phase space with 1 configuration space dimension and 1 velocity space dimension, to full 6D phase space with 3 configuration space dimensions and 3 velocity space dimensions).
• Took ~123 seconds for Lanyon to generate everything.
  • ~10 seconds for the electrostatic Vlasov equation in 1x1v, ~15 seconds for the electrostatic Vlasov equation in 1x2v, ~21 seconds for the electrostatic Vlasov equation in 1x3v, ~17 seconds for the electrostatic Vlasov equation in 2x2v, ~32 seconds for the electrostatic Vlasov equation in 2x3v, and ~28 seconds for the electrostatic Vlasov equation in 3x3v.
  • Real-time screen captures are shown in /screencaps.
• 18,589 lines of Lean 4 code to prove end-to-end correctness properties.
  • 1,101 for the electrostatic Vlasov equation in 1x1v, 2,039 for the electrostatic Vlasov equation in 1x2v, 3,313 for the electrostatic Vlasov equation in 1x3v, 2,747 for the electrostatic Vlasov equation in 2x2v, 4,216 for the electrostatic Vlasov equation in 2x3v, 5,173 for the electrostatic Vlasov equation in 3x3v.
• 450 total definitions and 312 total theorems.
• 12,143 lines of formally verified C code.
  • 856 for the electrostatic Vlasov equation in 1x1v, 1,414 for the electrostatic Vlasov equation in 1x2v, 2,100 for the electrostatic Vlasov equation in 1x3v, 1,880 for the electrostatic Vlasov equation in 2x2v, 2,653 for the electrostatic Vlasov equation in 2x3v, and 3,240 for the electrostatic Vlasov equation in 3x3v.

The most general form of the electrostatic Vlasov equation for a single (charged) particle species ${\alpha}$ is:

$$ \frac{\partial f_{\alpha}}{\partial t} + \mathbf{v}_{\alpha} \cdot \frac{\partial f_{\alpha}}{\partial \mathbf{x}} + \frac{q_{\alpha} \mathbf{E}}{m_{\alpha}} \cdot \frac{\partial f_{\alpha}}{\partial \mathbf{v}} = 0 $$

for one-particle distribution function ${f_{\alpha}}$, configuration space coordinates ${\mathbf{x}}$, velocity space coordinates ${\mathbf{v}}$, particle charge ${q_{\alpha}}$, particle mass ${m_{\alpha}}$, and electric field ${\mathbf{E}}$. This is often made self-consistent by coupling to the Poisson equation:

$$ \nabla^2 \phi + \frac{\rho}{\varepsilon} = 0 $$

for electrostatic potential ${\phi}$, electric charge density ${\rho}$, and electric permittivity ${\varepsilon}$, to obtain the Vlasov-Poisson system. In this particular case, however, we consider a fixed electrostatic potential only, and leave rigorous investigation of the full Vlasov-Poisson system for a future Lanyon research note!