Designing Typeclasses in Mathlib: Abstraction, Inference, and Reuse

报告人：赵雨扬（香港中文大学（深圳））

时  间：2026年9月1日 16:00

地  点：海韵园实验楼S102

内容摘要:

Mathlib is one of the largest libraries of formalized mathematics in the Lean ecosystem. To make theorems reusable across groups, rings, modules, ordered structures, and many other settings, Mathlib relies extensively on typeclasses to represent structures, properties, and the relationships among them. Through representative examples, this talk introduces typeclasses, instances, and instance search, and explains how Mathlib organizes mathematical knowledge through structure hierarchies, minimal assumptions, and automated inference. We will also examine how poorly designed instances can create ambiguity, search overhead, and maintenance difficulties, and how a large mathematical library balances usability, performance, and extensibility. The broader message is that formalizing mathematics is not only about encoding proofs: it also requires the careful design of reusable mathematical interfaces.

个人简介：

赵雨扬，香港中文大学（深圳）人工智能学院与深圳河套学院联合培养博士生，长期参与 Lean 开源社区和 Mathlib 建设。自 2021 年起，他已为 Mathlib 贡献数百个 Pull Request，并获 2025 年 CCF 首届定理证明竞赛一等奖第二名。他关注类型类推断、数学库维护及形式化证明实践。

联系人：马家骏