Abstract : This talk presents methods for interacting and querying Lean's mathematical library, Mathlib. Users unfamiliar with the library may find it difficult to determine how statements should be phrased in Mathlib's terminology, or may not know how to find whether a result they are interested in appears in the library. We will present techniques for addressing these issues is a somewhat systematic fashion by means of a series of examples.

Keywords : Lean; Mathlib; formalization