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.
The direct detection of gravitational waves by LIGO has confirmed general relativity (GR) and sparked rapid growth in gravitational wave (GW) astronomy. However, subtle post-Newtonian (PN) deviations observed during the analysis of high …
Novel background metric expansion method for constructing rotating charged black hole solutions in higher-dimensional Kaluza-Klein supergravity with (anti-)de Sitter spacetime.