← All papers
Scalar actions in Lean's mathlib
cs.LO
Aug 10, 2021 · v1
TL;DR
Analyzes the typeclass-based encoding of scalar actions throughout Lean's mathlib library.
Abstract
Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. This paper explores how Lean 3's typeclasses are used by mathlib for scalar actions, illustrates problems including compatibility of actions and non-definitionally-equal diamonds, and notes solutions and areas still needing more work.
Problem
Scalar actions are ubiquitous in mathematics, but formalizing them concisely in a proof assistant raises issues with typeclass design, compatibility of actions, and non-definitionally-equal diamonds.
Approach
The paper explores how Lean 3 typeclasses are used by mathlib for scalar actions. It documents the design patterns, illustrates problems including compatibility of multiple actions on the same type and diamond inheritance issues where different paths yield non-definitionally-equal instances.
Results
The paper identifies key problems in mathlib scalar action design (compatibility conditions, non-definitional diamonds) and notes existing solutions along with areas still requiring more work.