This reposity is home to a small library of mathematics formalised in Lean 4. Inspired by other, more substantial, libraries such as Mathlib and the Agda Standard Library, this library does not hope to be comprehensive in any sense. Rather my aim with this code is to learn about the process of formalisation of mathematics in a functional language inspired by type theory. Lean, Agda, and Coq are examples of such languages.
First on the list of things to do is represent the number systems mathematicians are interested in. Including the natural numbers, integers, rationals, reals, and complex numbers. In the future finite fields, p-adic fields, and other (semi)rings should be defined. In parallel to this the hierachy of algebraic objects (groups, rings etc.) should be developed.