- End-to-end formally verified solvers for the ideal magnetohydrodynamics (MHD) equations, both with and without hyperbolic divergence cleaning (and assuming an ideal gas equation of state), in 1D, 2D, and 3D.
- Took ~434 seconds for Lanyon to generate everything.
- ~40 seconds for ideal magnetohydrodynamics in 1D, ~75 seconds for ideal magnetohydrodynamics in 2D, ~88 seconds for ideal magnetohydrodynamics in 3D, ~48 seconds for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 1D, ~74 seconds for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 2D, ~109 seconds for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 3D.
- 49,317 lines of Lean 4 code to prove end-to-end correctness properties.
- 4,004 for ideal magnetohydrodynamics in 1D, 7,806 for ideal magnetohydrodynamics in 2D, 11,678 for ideal magnetohydrodynamics in 3D, 4,399 for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 1D, 8,585 for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 2D, 12,845 for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 3D.
- 270 total definitions and 156 total theorems.
- 31,964 lines of formally verified C code.
- 2,628 for ideal magnetohydrodynamics in 1D, 5,064 for ideal magnetohydrodynamics in 2D, 7,542 for ideal magnetohydrodynamics in 3D, 2,881 for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 1D, 5,562 for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 2D, 8,287 for ideal magnetohydrodynamics (with hyperbolic divergence cleaning) in 3D.
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|