Overview
This project develops machine-checked mathematics for classical gravity and general relativity using Lean 4 and Mathlib. The goal is to turn definitions, calculations, and derivations from the physics literature into explicit mathematical statements and reusable proofs checked by Lean’s kernel.
Each result makes its assumptions visible: parameter restrictions, coordinate domains, nonvanishing denominators, and smoothness of the fields.
Research directions
- Exact spacetimes and coordinate transformations: verify metrics, curvature, vacuum equations, and relations between coordinate descriptions of classical solutions such as Schwarzschild and Kerr.
- Einstein–Maxwell systems: certify charged backgrounds and first variations, and connect linearized equations to Kerr–Newman radiation systems.
- Black-hole perturbations: check explicit changes of variables, matrix integrating factors, and equivalences between perturbation systems, building foundations for further work on separation and stability.
The Prove2Me profile collects the Exact Vacuum Atlas and Exact Spacetime Atlas missions. Individual mission pages record their precise targets, proof dependencies, and progress.
Standalone formalization
Hintz2026: Local Equivalence of Kerr–Newman Perturbation Systems is a separately published result within this research direction, with its own Lean source, pinned dependencies, and reproduction instructions.
中文简介
本项目使用 Lean 4 与 Mathlib，逐步形式化经典引力中的精确时空、坐标变换、Einstein–Maxwell 系统和黑洞扰动方程，明确每项结论的假设与适用区域。任务与进展汇总于 Prove2Me；Hintz2026 是其中独立发布的局部等价证明成果。
