Organizational features

5. Organizational features#

Lean helps organize formalized mathematics in several ways. In this lecture we shall look at three mechanisms:

5.1. Formalization styles#

In the remaining time we will practice different formalization styles, from directly writing proof terms to using varying amounts of tactics.

5.2. Reading material#

5.3. Homework#

  • Continue going through Mathematics in Lean, and make sure you solve exercises!

  • Browse Mathlib (the Mathlib section) too see what is already there.

  • Think about what you would like to formalize for your class project. It should be a topic that you are familiar with, and it should have several good goal posts, so that if you do not reach the end you will still have accomplished something.

5.4. Video#

Contents