“In my entire scientific life, extending over forty-five years, the most shattering experience has been the realization that an exact solution of Einstein's equations of general relativity, discovered by the New Zealand mathematician, Roy Kerr, provides the absolutely exact representation of untold numbers of massive black holes that populate the universe.”
This site is a mathematical relativity database centred on Kerr and Kerr-related rotating black-hole models. The mathematics of exact Kerr is a benchmark, but many entries concern near-Kerr vacuum dynamics, Kerr–Newman, Kerr–de Sitter, Kerr–AdS, or near-horizon (NHEK) limits. Those settings differ in asymptotics, field content, and PDE boundary conditions — they are tagged explicitly so problems are not misread as interchangeable “Kerr” questions.
A parallel axis is formal verification: which statements have structured, finite-dimensional, or ODE-level content that proof assistants can plausibly attack first? Every problem records heuristic FV suitability and a short reason.
How to read this database
- Five clusters (Exterior stability, Interior / SCC, Extremal, Rigidity / Uniqueness, Spectral / scattering) organize research themes. They are intentionally coarse.
- Orthogonal tags (family, asymptotics, coupling, equation level, regime) say what geometry and PDE class the statement belongs to, independent of cluster placement.
- Relevance marks pure mathematics vs mixed vs physics-facing motivation (still rigorous statements — not observational claims).
- The formal verification track highlights math-leaning problems (including K-501–K-510) suited to early prover efforts.
Orthogonal tags (quick reference)
- Theorem status
- Open / partial / conditional / solved / needs review — solution progress, orthogonal to problem type.
- Problem type
- Classical frontier vs quantitative sharpening vs formalization target, etc.
- Research state
- Literature-solved vs open-in-literature vs high-value unformalized / synthesized targets.
- Family
- Exact Kerr vs near-Kerr vacuum vs Kerr–Newman, Λ ≠ 0, NHEK, or broader rotating families.
- Asymptotics
- Asymptotically flat, de Sitter, AdS, or mixed settings (not interchangeable).
- Coupling
- Vacuum Einstein vs matter-coupled (e.g. Einstein–Maxwell).
- Equation level
- Scalar/Maxwell/linearized gravity/full Einstein, reductions, spectral operators, inverse problems.
- Regime
- Stationary vs dynamical; linear vs nonlinear; exterior/interior; extremal/near-extremal.
- Relevance
- Pure math vs mixed vs physics-facing motivation.
- FV suitability
- Heuristic formal-verification friendliness (high / medium / low) with a short reason on each problem.
Flagship open problems
Open entries rated difficulty ≥ 4 (heuristic).
Most formalization-friendly
High FV suitability (see FV track).
Recently updated
All problems · Formal verification · Methodology & status taxonomy · Contribute · About