Structuring Definitions in Mathematical Libraries
Alena Gusakov, Peter Nelson, Stephen Watt
TL;DR
The paper addresses the challenge of structuring mathematical definitions in formal libraries, highlighting how choices in definitions shape usability and automation. It analyzes Lean's dependent type theory and presents case studies of continuous functional calculus, graded rings, matroids, and graphs to illustrate practical design patterns and pitfalls. It compares experiences with computer algebra systems (e.g., Aldor) to identify language-library interactions, proposing design strategies like 'junk value' interfaces, outParam predicates, carrier-set hierarchies, and layered constructors. The findings provide practical guidance for building scalable, readable, and extensible mathematical libraries in proof assistants and CAS.
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.