Structuring Definitions in Mathematical Libraries
Alena Gusakov, Peter Nelson, Stephen Watt
cs.SC
Sep 13, 2025 · v1
TL;DR
Surveys, with mathlib case studies, what makes a formal definition "good" when added to the Lean library.
Abstract
Codifying mathematical theories in a proof assistant or computer algebra system is a challenging task, of which the most difficult part is, counterintuitively, structuring definitions. This results in a steep learning curve for new users and slow progress in formalizing even undergraduate level mathematics. There are many considerations one has to make, such as level of generality, readability, and ease of use in the type system, and there are typically multiple equivalent or related definitions from which to choose. Often, a definition that is ultimately selected for formalization is settled on after a lengthy trial and error process. This process involves testing potential definitions for usability by formalizing standard theorems about them, and weeding out the definitions that are unwieldy. Inclusion of a formal definition in a centralized community-run mathematical library is typically an indication that the definition is "good." For this reason, in this survey, we make some observations about what makes a definition "good," and examine several case studies of the refining process for definitions that have ultimately been added to the Lean Theorem Prover community-run mathematical library, mathlib. We observe that some of the difficulties are shared with the design of libraries for computer algebra systems, and give examples of related issues in that context.
Problem
Structuring definitions in proof assistants and computer algebra systems is surprisingly difficult, resulting in a steep learning curve and slow progress in formalizing even undergraduate-level mathematics. There are many considerations (generality, readability, type system usability) and typically multiple equivalent definitions to choose from.
Approach
The authors survey what makes a definition 'good' in mathematical libraries, examining several case studies of the refining process for definitions that have been added to Lean's mathlib. They compare the challenges with analogous issues in computer algebra system library design. The study covers considerations such as level of generality, readability, and ease of use in the type system.
Results
The paper identifies shared difficulties between proof assistant and computer algebra system library design. It provides concrete observations and advice for structuring definitions, drawing on examples from mathlib where definitions were settled after lengthy trial and error processes involving testing by formalizing standard theorems.
