Teaching a class on Analysis I with Lean outside academia?

Stream: Analysis I

[Rado Kirov]

I am toying with the idea of teaching a class on the material of chapter 1 to 5 to interested folks in the bay area (likely mostly software people.) I wrote up proposal syllabus https://docs.google.com/document/d/1bCJ9Y_Y13A65kJUHgvzI8_3GMCVL5Ys55m4Qoz0G8CA/edit?tab=t.0#heading=h.2ds6n3ym2aob

any thoughts, comments, suggestions (anyone can comment in the doc) before I start looking for participants?

My hypothesis is that there are at least 10-20 software engineers in the bay area that are math-curious (like @Dan Abramov :) too bad you are in London) and Lean actually makes their foray into proofs more interesting and pleasant given they are used to using computers to write code.

[Terence Tao]

This sounds like a great idea! I'd be happy to use this space as a forum for students in this class to discuss the Lean-related topics arising in the class (presumably any purely administrative questions of interest only to class participants should go elsewhere though).

[Rado Kirov]

I sent the word out on the social media channels - https://bsky.app/profile/radokirov.bsky.social/post/3lzko27svuk2b etc. So let's see how it goes.

I'd be happy to use this space as a forum for students in this class to discuss the Lean-related topics arising in the class

Yes, my plan was to do a first pass in a dedicated discord channel and "upstream" here questions that I struggle to answer well.

[Rado Kirov]

Got 11 interest responses so far, so this is a go interest-wise, next steps figure out the venue.

[Rado Kirov]

Big thanks to everyone here boosting the message!

[Rado Kirov]

We got a venue in San Francisco and will do the first meetup next Monday. Got 16 replies on the interest form and some participation in the discord forum.

[Alok Singh]

What's the venue?

[Rado Kirov]

Moxsf

[Alok Singh]

lol of course. How did you find it

[Rado Kirov]

Someone had an algebra and cat theory there earlier in the year. Didn’t have any other options realistically. I was more hopeful for tech companies having event space to share but couldn’t find any.

[Alok Singh]

Relax dude, I don’t think you could do better than mox

[Greg Shuflin]

I just saw this thread - I'm definitely interested in this real analysis thing, although I'm not sure if i can consistently commit to it with my work schedule. I'm curious if this ended up happening or if it's possible to join late @Rado Kirov

[Rado Kirov]

Not to late at all, we met 3-4 times only so far and most people are still on NNG or chapter 2. Just join the discord https://discord.com/invite/bXNPhQyjfe to get the rest of the details.