Formal verification & math-leaning problems

This site is primarily a mathematical relativity problem database. Formal proof assistants (Lean, Coq, Isabelle, …) are most effective when statements have clear boundaries: finite-dimensional data, commuting operators, algebraic tensor identities, or separated ODEs with explicit parameters.

Orthogonal tags mark fv_suitability (high / medium / low) with a short fv_reason on every problem. These are heuristics, not judgments about intrinsic importance.

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.

Why some Kerr problems formalize more easily

Exact / stationary / symmetry-rich backgrounds reduce the problem to algebra, ODEs, or elliptic PDE on lower-dimensional domains.
Separable modes and spectral edges produce countable families of inequalities with checkable hypotheses.
Finite-dimensional rigidity (tensors, horizon data, Carter-type operators) maps naturally to dependent-type formalization.
Explicit tensor identities (Mars–Simon, Killing–Yano, Ernst reductions) are textbook material for proof libraries.

What to defer. Full K-001-style nonlinear stability of subextremal Kerr is a global Einstein PDE program. It remains scientifically central, but it is a poor first formalization target: too many moving parts (gauge, modulation, trapping, radiation) for an initial library unless aggressively scoped to lemmas.

Best first targets

High FV suitability; emphasis on algebra, ODEs, and stationary reductions. Includes the curated track K-501–K-510.

K-501 — Quantitative Mars–Simon tensor gap for near-Kerr stationary vacuum data · Pure math
K-502 — Horizon-data rigidity and effective reconstruction of Kerr parameters · Pure math
K-503 — Algebraic uniqueness of quadratic symmetry operators commuting with $\Box_g$ on exact Kerr ($\mathcal{D}_{\le 2}$ class) · Pure math
K-504 — Quantitative stability of the photon region and spherical null geodesics under near-Kerr perturbations · Pure math
K-505 — Threshold phenomena in separated Teukolsky-type ODEs on Kerr (zero modes, algebraically special limits, superradiant edges) · Pure math
K-506 — High-frequency Kerr quasinormal-mode laws with explicit remainder bounds · Pure math
K-507 — Finite-data inverse resonance recovery of Kerr parameters · Mixed
K-508 — Stability or obstruction for approximate Killing–Yano tensors near Kerr · Pure math
K-509 — Charge–tail correspondence in the extremal limit · Mixed
K-510 — Ernst equation on stationary axisymmetric vacuum exteriors — sharp uniqueness class for asymptotically flat Kerr (boundary-value formulation) · Pure math
K-004 — Peeling and polyhomogeneous expansions at null infinity for nonlinear near-Kerr evolutions FV: high
K-007 — Einstein–Maxwell stability near Kerr FV: high
K-105 — Critical horizon-decay exponent controlling extendibility FV: high
K-108 — Strong cosmic censorship in rotating $\Lambda>0$ black-hole interiors (conditional on a spectral–interior bridge) FV: high
K-205 — Rigorous near-horizon scattering theory for NHEK FV: high
K-208 — Near-extremal QNM accumulation and branch-cut structure FV: high
K-303 — Quantitative Kerr characterization via the Mars–Simon tensor FV: high
K-304 — Near-Kerr rigidity with computable geometric constants FV: high
K-305 — Kerr characterization from horizon intrinsic data FV: high
K-401 — QNM completeness for Kerr ringdown expansions FV: high
K-407 — QNM excitation factors and universality theorems FV: high
K-634 — Classify all second-order symmetry operators commuting with the scalar wave operator on Kerr. FV: high

Intermediate targets

Medium suitability: still structured, but microlocal remainders, coupled fields, or parameter uniformity add cost.

K-002 — Uniform nonlinear stability as $a \to M^-$
K-003 — Nonlinear asymptotic completeness near Kerr
K-005 — Sharp nonlinear Price law for curvature
K-006 — Kerr stability with BMS charges and nonlinear memory
K-008 — Full asymptotically flat stability of the subextremal Kerr–Newman family
K-009 — Einstein–massive Klein–Gordon near Kerr: classification of stable and unstable regimes
K-010 — Nonlinear superradiant endstates in Kerr–AdS
K-011 — Spin fields on dynamical near-Kerr backgrounds

Long-term moonshots (illustrative)

Low FV suitability on this rubric — global dynamics, rough data, or open-ended modeling. Not “unimportant”; just poor first formalization objects.

K-001 — Full nonlinear stability of subextremal Kerr (Exterior Stability)
K-106 — Genericity of lower bounds for linearized-gravity interior instability (Interior / SCC)
K-112 — Teukolsky interior asymptotics beyond the current state of the art (Interior / SCC)
K-601 — Prove unconditional linear stability of Kerr (full subextremal range) in a fixed gauge, with full decay rates. (Exterior Stability)
K-602 — Prove nonlinear stability of Kerr for the full subextremal range |a|<M. (Exterior Stability)
K-603 — Prove nonlinear stability of Kerr with quantitative scattering (asymptotic completeness near Kerr). (Spectral / Scattering)
K-604 — Establish a sharp peeling/polyhomogeneity theorem at future null infinity ($\mathcal{I}^+$) for nonlinear near-Kerr evolutions. (Exterior Stability)
K-605 — Prove sharp nonlinear Price-law tails for curvature in near-Kerr vacuum. (Exterior Stability)

Browse all problems with FV filters · Metadata definitions