Naoki Takata
January 12, 2026
We present a formal specification of the Full Kerr Nonlinear Stability Conjecture in the Lean 4 proof assistant using the Mathlib library. The Kerr family of spacetimes describes rotating black holes in general relativity, and the nonlinear stability conjecture asserts that small perturbations of the initial data for a sub-extremal Kerr black hole evolve into spacetimes that remain close to and eventually settle down to a nearby Kerr solution. Our formalization provides a rigorous type-theoretic template that captures the essential mathematical structure of the conjecture, including the definitions of Kerr parameters, sub-extremal conditions, initial data manifolds, spacetime structure, and the stability-convergence properties. The formalization compiles successfully in Lean 4 and serves as a foundation for future detailed formalizations of general relativistic stability results.
As a proof of existence for this paper, the Keccak-256 hash of the PDF has been recorded on the Ethereum blockchain.
Timestamp: January 12, 2026 (date recorded on the blockchain)
The formalization is implemented in Lean 4.24.0 with Mathlib (commit f897ebcf). The statement FullKerrNonlinearStabilityConjectureStatement is verified to be a well-typed proposition by successful compilation.
Naoki Takata
X: @naokitakata
Email: [ntakata [at] proton.me]
This is a preprint. Comments are welcome!