Minimathlib: an experimental mathlib

Stream: Lean for teaching

[Daniel Levin]

Hi all,

I started hacking on a very early stage, very minimal project that aims to be an independent version of mathlib digestible to newcomers. I'm mainly working on this to teach _myself_ Lean. I don't anticipate it'll be of much use to anyone - and it is likely full of juvenile decisions - but in my experience throwaway projects like this tend to become useful once they pick up a bit of steam.

https://github.com/daniel-levin/Minimathlib

[suhr]

Starting with abstract definitions (like TopologicalSpace) rather than specific problems to solve/prove?

[Daniel Levin]

The abstract definitions only exist so that I can later define interesting theorems that can be dispatched with undergrad level mathematics. One of my goals is to make the statements of interesting theorems not just easy to understand but also relatively self-contained. That probably means a lot of 'flattened' type classes and a lot of time spent figuring out appropriate definitions.

[Daniel Levin]

My target audience is me: someone who has an undergraduate degree in mathematics and works as a programmer but has _no idea_ how to formalize mathematics

[suhr]

Proving some result is usually a good way to figure out all the definitions and lemmas you actually need.
And it usually turns out that you need a lot of lemmas.

[Rado Kirov]

Doing the exercises in https://github.com/teorth/analysis achieves a similar goal and has been my source of material to learn Lean. Especially chapter 2 and chapter 3 have self isolated Peano and ZFC set axiomatization not using mathlib along with basically every basic theorem you would like to proof for those.

[Rado Kirov]

We discuss those in #Analysis I btw