Formalization of Harder-Narasimhan Theory

Speaker: 袁轶君 / Yijun YUAN (西湖大学理论科学研究院 / Institute for Theoretical Sciences, Westlake University)

Time: 2025-11-19 15:00-16:00
Location: 1710, SIMIS

Abstract: The classical 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 work, 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.

---

About Speaker: Yijun Yuan obtained his Ph.D. degree from the Yau Mathematical Sciences Center at Tsinghua University in the current year. He is presently engaged as a postdoctoral fellow at the Institute for Theoretical Sciences, Westlake University. His research focuses on p-adic Galois representations, p-adic transcendental number theory, and the formalization of arithmetic geometry.