Zulip Chat Archive

Stream: new members

Topic: Dependencies of the chapters of the math in lean book


Michael Novak (Sep 27 2025 at 09:57):

Hi, I've been learning lean from the math in lean book for a few weeks, and I finished the first 3 chapters ( introduction, basics, logic). It seems like they are the more foundational chapters that are needed for anyone that uses lean to prove mathematical theorems and most of the other chapters are more about showcasing theorem proving in specific math subjects (perhaps with the exception of the fourth chapter which is about set theory and functions? although lean is based on type theory, so I think sets are not really foundational, right?).
I was wondering if one could learn whichever chapters one is interested in after the first 3 chapters, or are there any dependencies between the chapters. And also, if there aren't any dependencies, is there some order which is more optimal pedagogically?


Last updated: Dec 20 2025 at 21:32 UTC