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

翻译：哈德-纳拉辛汉理论为射影曲线上的向量丛提供了一个典范滤过，其逐次商是半稳定的且具有严格递减的斜率。在本文中，我们在证明辅助工具Lean 4与Mathlib中展示了哈德-纳拉辛汉理论的形式化。该形式化基于陈和让南近期对哈德-纳拉辛汉理论的一种新方法，该方法以序论术语重新诠释了该理论，并避免了经典理论对代数几何的依赖。作为应用，我们形式化了诺特环上有限生成模的准素滤过的唯一性，以及半稳定哈德-纳拉辛汉博弈的若尔当-赫尔德滤过的存在性。代码可见于：https://github.com/YijunYuan/HarderNarasimhan