AI-assisted formalization in Lean 4 / Mathlib of the main results of Bridgeland's Stability conditions on triangulated categories (Annals of Mathematics, 2007).
Inspired by Douglas's work on Π-stability in string theory, Bridgeland
showed that the classical stability package — central charges, semistable
objects, Harder-Narasimhan filtrations — can be lifted from abelian categories
to triangulated categories. A Bridgeland stability condition on a triangulated
category D consists of a central charge Z : K₀(D) → ℂ and a slicing
P(φ) into semistable objects of each phase, subject to compatibility and
Harder-Narasimhan existence axioms.
The headline result is that the space Stab(D) of all such conditions is
itself a complex manifold, with local charts given by the central charge.
The theory has since become one of the most active areas in modern
mathematics. It provides infrastructure for wall-crossing in birational
geometry, Donaldson-Thomas theory, and the study of moduli spaces of sheaves
on surfaces and threefolds.
The formalization covers Sections 2–7 of the paper, culminating in:
- Theorem 1.2 — the central charge map is a local homeomorphism on each
connected component of
Stab(D). - Corollary 1.3 — connected components of
Stab_N(D)are finite-dimensional complex manifolds.
Both are proved for an arbitrary surjective class map v : K₀(D) →+ Λ and
specialized to the identity (Theorem 1.2) and the numerical quotient
(Corollary 1.3). The formalization works in class-map generality as in
Bayer–Macrì–Stellari [8, Appendix A] and Bayer–Lahoz–Macrì–Nuer–Perry–Stellari
[11], where the central charge factors through a surjection v : K₀(D) →+ Λ;
the classical Stab(D) is the specialization v = id.
- Project website — informal mathematical descriptions of each declaration, with a table of paper statements that currently have exact formal analogs.
- API docs — auto-generated Lean API documentation (doc-gen4).
- Comparator Manual — independent verification of the formal statements against their source, listing the trusted base you must audit to trust the proof.
The root import is BridgelandStability.lean.
This is an experiment in AI-assisted formalization.
Rule 1: Humans write no Lean code beyond Mathlib. The goal is to study how far a human-led effort can push AI-assisted formalization on top of Mathlib.
Rule 2: Getting Lean to accept a proof script is not success. The end state has to be Mathlib quality: correct abstractions, reusable lemmas, sane names, controlled imports, and proofs that could plausibly survive code review and upstreaming.
- Michael R. Douglas, D-branes, Categories and N=1 Supersymmetry, J. Math. Phys. 42 (2001), 2818-2843.
- Tom Bridgeland, Stability conditions on triangulated categories, Annals of Mathematics 166 (2007), 317-345.
- Tom Bridgeland, Stability conditions on K3 surfaces, Duke Mathematical Journal 141 (2008), 241-291.
- Daniele Arcara and Aaron Bertram, Bridgeland-stable moduli spaces for K-trivial surfaces, Journal of the European Mathematical Society 15 (2013), 1-38.
- Arend Bayer and Emanuele Macrì, Projectivity and birational geometry of Bridgeland moduli spaces, Journal of the American Mathematical Society 27 (2014), 707-752.
- Arend Bayer and Emanuele Macrì, MMP for moduli of sheaves on K3s via wall-crossing: nef and movable cones, Lagrangian fibrations, Inventiones mathematicae 198 (2014), 505-590.
- Tom Bridgeland and Ivan Smith, Quadratic differentials as stability conditions, Publications mathematiques de l'IHES 121 (2015), 155-278.
- Arend Bayer, Emanuele Macrì, and Paolo Stellari, The space of stability conditions on abelian threefolds, and on some Calabi-Yau threefolds, Inventiones mathematicae 206 (2016), 869-933.
- Arend Bayer, A short proof of the deformation property of Bridgeland stability conditions, preprint, 2016.
- Marcello Bernardara, Emanuele Macrì, Benjamin Schmidt, Xiaolei Zhao, Bridgeland Stability Conditions on Fano Threefolds, EpiGA 1 (2017), article 8.
- Chunyi Li, On stability conditions for the quintic threefold, Inventiones mathematicae 218 (2019), 301-340.
- Arend Bayer, Martí Lahoz, Emanuele Macrì, Howard Nuer, Alexander Perry, Paolo Stellari, Stability conditions in families, Publications mathematiques de l'IHES 133 (2021), 157-325.
- Soheyla Feyzbakhsh and Richard P. Thomas, Rank r DT theory from rank 1, Journal of the American Mathematical Society 36 (2023), 795-826.
- Soheyla Feyzbakhsh and Richard P. Thomas, Rank r DT theory from rank 0, Duke Mathematical Journal 173 (2024), 2063-2116.
- Soheyla Feyzbakhsh, Naoki Koseki, Zhiyu Liu, Nick Rekuski, Stability conditions on Calabi-Yau threefolds via Brill-Noether theory of curves, preprint, 2025.
- Chunyi Li, A Remark on Stability Conditions on Smooth Projective Varieties, preprint, 2026.