Lean and the Mathematics Library

Lean is a programming language as well as being a theorem prover. It powers everything, but lean itself knows barely any mathematics at all. Cauline just needs the absolute basic to be a programming language. So where does the mathematics go? Well, in 20 17, they decided that this new mathematics library was born. T was called mathlib, lean's mathematics library.