AxiomMath
IMO2026
AxiomProver is an autonomous multi-agent ensemble theorem prover for Lean 4 that achieved a perfect score at IMO 2026 by solving all six problems.
Why it is worth attention
Demonstrates end-to-end formal verification of complex physics simulations, generating 24,614 lines of Lean 4 code and 11,730 lines of verified C code automatically in about 340 seconds.
Who it is for
- Researchers in numerical relativity and computational astrophysics
- Formal verification engineers and theorem proving enthusiasts
- Physicists studying electrodynamics in curved spacetime
- Developers of automated code generation and verification tools
Use cases
- Simulating electromagnetic fields around black holes and other compact objects
- Verifying numerical methods for solving Maxwell's equations in general relativity
- Teaching formal verification applied to scientific computing
- Benchmarking automated theorem proving systems for real-world equations
Strengths
- Covers 1D, 2D, and 3D formulations with both standard and divergence-corrected equations
- Explicit lines of code and generation time provided (e.g., 86 seconds for 3D PH GRM equations)
- End-to-end verified pipeline from mathematical equations to executable C code
- Includes 156 total theorems and 270 definitions across the generated code
Considerations
- Generated code relies on the Lanyon system, which may not be publicly available or easily reproducible
- Performance characteristics of the verified C code compared to hand-optimized solvers are not discussed
- Limited to the ADM decomposition formalism; other formulations of GRMHD are outside scope
README quick start
General Relativistic Maxwell Equations for Curved Spacetime Electrodynamics with Lanyon
Highlights
- End-to-end formally verified solvers for the general relativistic Maxwell equations and perfectly hyperbolic general relativistic Maxwell equations (with electric and magnetic divergence error correction), for electrodynamics in curved spacetime, in 1D, 2D, and 3D.
- Took ~340 seconds for Lanyon to generate everything.
- ~31 seconds for the general relativistic Maxwell equations in 1D, ~54 seconds for the general relativistic Maxwell equations in 2D, ~71 seconds for the general relativistic Maxwell equations in 3D, ~37 seconds for the perfectly hyperbolic general relativistic Maxwell equations in 1D, ~61 seconds for the perfectly hyperbolic general relativistic Maxwell equations in 2D, ~86 seconds for the perfectly hyperbolic general relativistic Maxwell equations in 3D.
- Real-time screen captures are shown in
/screencaps.
- 24,614 lines of Lean 4 code to prove end-to-end correctness properties.
- 1,966 for the general relativistc Maxwell equations in 1D, 3,710 for the general relativistic Maxwell equations in 2D, 5,532 for the general relativistic Maxwell equations in 3D, 2,342 for the perfectly hyperbolic general relativistic Maxwell equations in 1D, 4,440 for the perfectly hyperbolic general relativistic Maxwell equations in 2D, 6,624 for the perfectly hyperbolic general relativistic Maxwell equations in 3D.
- 270 total definitions and 156 total theorems.
- 11,730 lines of formally verified C code.
- 1,001 for the general relativistic Maxwell equations in 1D, 1,798 for the general relativistic Maxwell equations in 2D, 2,641 for the general relativistic Maxwell equations in 3D, 1,150 for the perfectly hyperbolic general relativistic Maxwell equations in 1D, 2,080 for the perfectly hyperbolic general relativistic Maxwell equations in 2D, 3,060 for the perfectly hyperbolic general relativistic Maxwell equations in 3D.
Further Details
In a generic curved spacetime (decomposed into spacelike hypersurfaces via the ADM decomposition), the general relativistic Maxwell equations of covariant electromagnetism combine a pair of hyperbolic evolution equations:
$$ \frac{\partial \mathbf{B}}{\partial t} + \nabla \times \left( \alpha \mathbf{D} + \boldsymbol\beta \times \mathbf{B} \right) = 0 $$
$$ \frac{\partial \mathbf{D}}{\
Description
End-to-end formally verified solvers for the general relativistic Maxwell and perfectly hyperbolic general relativistic Maxwell equations in curved spacetime, in 1D, 2D, and 3D.
Related repositories
Similar projects matched by category, topics, and programming language.