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