mathlib

Lean's mathlib is where the mathematical community's formalizations of lots of different parts of mathematics live. There are riches here, for almost any application.

The upshot for you at this point is that, once you master the next part of the course, on predicate logic in Lean 4, you can pick nearly any area of mathematics and reason in it, now with the full support of Lean, its infrastructure, and vibrant community.

The great thing is that, unlike first-order theory, Lean admits the practical, abstract, expressive, and verified embedding of an incredible diversity of logical and mathematical structures into its foundational logic, formulated in the abstract concepts of the mathematical domains, and made much more useful with concrete notations appropriate to the particular field being formalized. In Lean, one can speak easily about such things as properties of relations, or real real numbers. Neither is possible in the first-order that we mostly teach in traditional courses.

Make no mistake, first-order predicate logic with first-order theory of sets and relations is still an utterly indispensable language. It's syntax is used in many important reasoning systems, incluiding Z3, Dafney, Alloy, and others. But with knowledge of Lean, you also have immediate access to this incredible treasure trove of verified mathematical knowledge, and it's nearly trivial to understand first-order logic once you have seen the bigger picture.

If you're interested in a visual overview of areas of mathematics that Lean 4's mathlib provides, the overview of mathlib in Lean 3 is the best right now. The Lean 4 version is evolving and contributions are welcome.