The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.
Amazon（亚马逊）；Stanford University（斯坦福大学）；Google DeepMind（谷歌DeepMind）；The University of Texas at Austin（德克萨斯大学奥斯汀分校）；FORM, University of Southern Denmark（南丹麦大学FORM）；Lean FRO；Atlas Computing（阿特拉斯计算）；Getulio Vargas Foundation（热图利奥·瓦加斯基金会）；Institute for Theoretical Studies, ETH Zürich（苏黎世联邦理工学院理论研究所）
Université Paris Cité and Sorbonne Université, CNRS, IMJ-PRG（巴黎西岱大学与索邦大学，法国国家科学研究中心，数学与计算机研究所）；Université Paris Cité, CNRS, Institut de recherche en informatique fondamentale（巴黎西岱大学，法国国家科学研究中心，基础信息学研究所）
New York University（纽约大学）；Aarhus University（奥胡斯大学）；ETH Zurich（苏黎世联邦理工学院）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究所）；Chalmers（查尔姆斯理工大学）
From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory
School of Data Science, The Chinese University of Hong Kong, Shenzhen（香港中文大学深圳数据科学学院）；School of Science and Engineering, The Chinese University of Hong Kong, Shenzhen（香港中文大学深圳科学与工程学院）
LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
Yau Mathematical Sciences Center, Tsinghua University（清华大学尤洋数学科学中心）；Iluvatar CoreX；Department of Mathematics, Southern University of Science and Technology（南方科技大学数学系）；Westlake Institute for Advanced Study, Westlake University（西湖研究学院）；Qiuzhen College, Tsinghua University（清华大学齐臻学院）；Department of Physics, The Chinese University of Hong Kong（香港中文大学物理系）；Yanqi Lake Beijing Institute of Mathematical Sciences and Applications (BIMSA)（燕琦湖北京应用数学研究所（BIMSA））
MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
Department of Computer Science, University of Virginia（弗吉尼亚大学计算机科学系）；Astronomy , California Institute of Technology（加州理工学院天文学系）；Purdue University（普渡大学）；Massachusetts Institute of Technology（麻省理工学院）
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
Georgia Institute of Technology（佐治亚理工学院）；University of Pennsylvania（宾夕法尼亚大学）；Foothill College（山麓学院）；Rutgers University（罗格斯大学）；Simon Fraser University（西蒙弗雷泽大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
University of Toronto（多伦多大学）；Computer Science Department, University of California, Los Angeles（加州大学洛杉矶分校计算机科学系）；Department of Computer Science, University College London（伦敦大学学院计算机科学系）；Google（谷歌）；Department of Mathematics and Computer Science, Rutgers University – Newark（罗格斯大学纽瓦克分校数学与计算机科学系）
