@lanyon_ai

Formally verified magnetohydrodynamics, with provably hyperbolicity-preserving magnetic divergence error correction. Simulating plasma vortices and supersonic plasma flows in arbitrary geometries using shock-capturing schemes for the equations of ideal MHD, all implemented and verified autonomously with Lanyon. ~32,000 lines of C, ~50,000 lines of Lean proof, ~150 correctness theorems, all generated in ~7 minutes. The ideal MHD equations couple the equations of hydrodynamics with Maxwell’s equations for electromagnetism to describe the interactions of perfectly conducting fluids with magnetic fields. As an elegant reduced-order description, the ideal MHD equations occur ubiquitously throughout heliophysics, geophysics, and astrophysical plasma physics, as well as in modeling the equilibrium and stability of nuclear fusion reactors. Solving these equations involves unique numerical and algorithmic challenges, including issues surrounding the preservation of divergence constraints for the magnetic field, as well as complex thermodynamic stability and wave-speed restrictions. Lanyon one-shotted an end-to-end formally verified solver for the ideal MHD equations, including a provably hyperbolicity-preserving divergence correction scheme based on the Dedner et al. approach, with fully executable mathematical, physical, and numerical correctness proofs. Then it ran a variety of complex numerical and physical validation simulations, and autonomously analyzed the results. To the best of our knowledge, this is the first ever fully formally verified divergence correction scheme for the MHD equations. GitHub link and technical deep dive below.👇 --- Technical deep dive by @minmodammar: https://lanyon.ai/research/ideal-mhd/… Corresponding GitHub repository: https://github.com/lanyonai/idealMHD…