← All papers
Formalization of Harder-Narasimhan theory
math.AG
Sep 23, 2025 · v1
TL;DR
Formalizes Harder-Narasimhan theory in Lean 4 with Mathlib via an order-theoretic reformulation avoiding algebraic geometry.
Abstract
The Harder-Narasimhan theory provides a canonical filtration of a vector bundle on a projective curve whose successive quotients are semistable with strictly decreasing slopes. In this article, we present the formalization of Harder-Narasimhan theory in the proof assistant Lean 4 with Mathlib. This formalization is based on a recent approach of Harder-Narasimhan theory by Chen and Jeannin, which reinterprets the theory in order-theoretic terms and avoids the classical dependence on algebraic geometry. As an application, we formalize the uniqueness of coprimary filtration of a finitely generated module over a noetherian ring, and the existence of the Jordan-Hölder filtration of a semistable Harder-Narasimhan game. Code available at: https://github.com/YijunYuan/HarderNarasimhan
Problem
Harder-Narasimhan theory, which provides canonical filtrations of vector bundles with semistable successive quotients of strictly decreasing slopes, has not been formalized in a proof assistant despite its importance in algebraic geometry.
Approach
The formalization in Lean 4 with Mathlib follows Chen and Jeannin's recent order-theoretic reinterpretation of Harder-Narasimhan theory, which avoids classical dependence on algebraic geometry. The approach works at the level of abstract ordered structures rather than vector bundles directly.
Results
The formalization covers Harder-Narasimhan theory and, as an application, proves the uniqueness of coprimary filtration of a finitely generated module over a principal ideal domain in Lean 4.