Smooth manifolds

Stream: maths

[bmitc]

I am new to Lean and am considering a project of working through some books and exercises on smooth manifolds and other such early level graduate topics in Lean, proving statements in the book(s) and also exercises and problems. This is to recall math I've forgotten, learn new math, and gain some new programming experience.

Where should I start aside from the obvious basics of learning bits of Lean 4? If I need to build my own library to handle Euclidean smooth manifolds and then general smooth manifolds, like Tu's book progresses, then that's fine. I'm just a little unsure where to start and see a lot of old talk about the generic manifold types not being ready, which isn't a huge concern of mine as I only care about real manifolds.

Assume familiarity with smooth manifolds at the level of Lee or Tu and experience in functional programming like F#, Elixir, Racket, other ML dialects, etc. but only an acquaintance with dependent types (I know what they are, just not much actual programming experience with them).

Thank you!

[Heather Macbeth]

@bmitc You could start with this overview of the manifolds library by @Oliver Nash -- it's from last year, so it's missing some of the latest developments and describes an older version of the language (Lean 3), but it gives a good overview of the design.