Machine-checked classical gravity with Lean 4 and Mathlib: exact spacetimes, coordinate transformations, and black-hole perturbation systems. Explore the formalization missions and progress on Prove2Me.
A standalone Lean 4 proof of the local equivalence between Kerr–Newman perturbation systems (1) and (7), for both spin signs, with reproducible source and an axiom audit.