Use and Abuse of Instance Parameters in the Lean Mathematical Library

Anne Baanen

doi:10.1007/s10817-024-09712-7

Use and Abuse of Instance Parameters in the Lean Mathematical Library

Anne Baanen^*

^*Corresponding author for this work

Computer Science

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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 finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.

Original language	English
Article number	1
Pages (from-to)	1-30
Number of pages	30
Journal	Journal of Automated Reasoning
Volume	69
Early online date	12 Dec 2024
DOIs	https://doi.org/10.1007/s10817-024-09712-7
Publication status	Published - 2025

Bibliographical note

Publisher Copyright:
© The Author(s) 2024.

Keywords

Algebraic hierarchy
Dependent type theory
Formalization of mathematics
Lean prover
Typeclasses

Access to Document

10.1007/s10817-024-09712-7

Persistent URL (handle)

Persistent link

Cite this

@article{c0ff629d774b46158df592ab77cea583,

title = "Use and Abuse of Instance Parameters in the Lean Mathematical Library",

abstract = "The Lean mathematical library Mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean{\textquoteright}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 finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.",

keywords = "Algebraic hierarchy, Dependent type theory, Formalization of mathematics, Lean prover, Typeclasses",

author = "Anne Baanen",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.",

year = "2025",

doi = "10.1007/s10817-024-09712-7",

language = "English",

volume = "69",

pages = "1--30",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

}

TY - JOUR

T1 - Use and Abuse of Instance Parameters in the Lean Mathematical Library

AU - Baanen, Anne

N1 - Publisher Copyright: © The Author(s) 2024.

PY - 2025

Y1 - 2025

N2 - 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 finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.

AB - 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 finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.

KW - Algebraic hierarchy

KW - Dependent type theory

KW - Formalization of mathematics

KW - Lean prover

KW - Typeclasses

UR - http://www.scopus.com/inward/record.url?scp=85211796120&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85211796120&partnerID=8YFLogxK

U2 - 10.1007/s10817-024-09712-7

DO - 10.1007/s10817-024-09712-7

M3 - Article

AN - SCOPUS:85211796120

SN - 0168-7433

VL - 69

SP - 1

EP - 30

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

M1 - 1

ER -

Use and Abuse of Instance Parameters in the Lean Mathematical Library

Abstract

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Use and Abuse of Instance Parameters in the Lean Mathematical Library

Cite this