KerrFormalization

KerrFormalization is an attempt to express important pieces of black-hole geometry in a form a proof assistant can check.

The work uses Lean to make definitions and arguments around Schwarzschild and Kerr spacetimes explicit, inspectable, and reusable.