The lean 4 theorem map is a snapshot of the lean 4 theorem proof assistant and the mathlib 4 library expressed as a derivation graph. The derivation graph shows all functions and theorems in the lean 4 and mathlib source files mapping from input types to output types. The input and output types are represented as nodes in the graph, and the functions/theorems are the edges.
