Bridgeland Stability Conditions
Inspired by Douglas's work on Π-stability in string theory, Bridgeland stability conditions allow one to extract a complex manifold from a triangulated category. A stability condition pairs a central charge — a group homomorphism from the Grothendieck group to the complex numbers — with a slicing of the category into semistable objects of each phase. Bridgeland's main theorem is that the space 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.
About this formalization
This site documents a machine-checked proof of the complex manifold theorem, formalized in Lean 4 using Mathlib. All Lean code is written by AI agents guided by human mathematicians — no human writes proof scripts. The formalization covers Sections 2–7 of Bridgeland's Stability conditions on triangulated categories (Annals of Mathematics, 2007), working in class-map generality as in Bayer–Macrì–Stellari and Bayer–Lahoz–Macrì–Nuer–Perry–Stellari.
Paper alignment
The table below lists every definition, lemma, and theorem from the paper that currently has an exact formal analog.
| Paper | Lean declaration |
|---|---|
| Theorem 1.2 | centralChargeIsLocalHomeomorphOnConnectedComponents |
| Corollary 1.3 | NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent |
| Definition 2.1 | StabilityFunction |
| Definition 2.2 | StabilityFunction.IsSemistable |
| Definition 2.3 | AbelianHNFiltration |
| Definition 3.3 | HNFiltration |
| Definition 4.1 | QuasiAbelian |
| Definition 4.4 | SkewedStabilityFunction |
| Definition 5.1 | PreStabilityCondition.WithClassMap |
| Lemma 5.2 | StabilityCondition.WithClassMap.P_phi_abelian |
| Definition 5.7 | StabilityCondition.WithClassMap |
| Lemma 6.1 | instPseudoEMetricSpaceSlicing |
| Lemma 6.2 | stabSeminorm_dominated_of_connected |
| Lemma 6.4 | StabilityCondition.WithClassMap.eq_of_same_Z_near |
| Theorem 7.1 | StabilityCondition.WithClassMap.deformation |
Why trust a proof written by AI?
Two independent checks. First, every logical step is verified by Lean's kernel — a small, fixed type checker that accepts or rejects proofs regardless of how they were produced. The kernel guarantees the arguments are correct. Second, the Comparator Manual lists the definitions the result depends on, paired with their informal mathematical meanings, so you can audit whether the formal statements faithfully capture the mathematics. Auto-generated API documentation is also available.
Contributing
Each declaration is paired with an informal description and, where available, a proof sketch. Passing the type checker is necessary but not sufficient: the formalization aims for Mathlib quality, with correct abstractions, reusable lemmas, and proofs that could survive code review and upstreaming. If you see a mathematical inaccuracy, a missing generalization, a cleaner definition, or — if you know Lean — a better proof strategy, each declaration has a link to open an issue. Describe what you think should happen and start a discussion. Once we figure out what needs to change, AI agents will do the rest.