Mathlib 贡献者

thumbnail.png

我从 2021 年开始将向 Lean 的官方数学库 Mathlib 贡献代码作为一项业余爱好。完成博士学位（2025 年）后，我目前再次成为活跃的常规贡献者。