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.
We review the state of the field of gravitational wave astrophysics, framing the challenges, current observations, and future prospects within the context of the predictions of Einstein's theory of general relativity.