Lean for Scientists and Engineers

Stream: Natural sciences

[Asei Inoue]

I would like to hear this, but I live in Japan and the time is midnight. Can I check the recordings and teaching materials later?

[Tyler Josephson ⚛️]

Thanks for your interest! When you register, you can share whether you plan to attend live or only want to check out the recordings afterwards.

[Shreyas Srinivas]

Is there a stream or a topic to discuss this?

[Notification Bot]

3 messages were moved here from #announce > Lean for Scientists and Engineers by Kevin Buzzard.

[Kevin Buzzard]

This thread is a better place than #announce for discussion/questions for the announcement here about Tyler's course on Lean for scientists and engineers. Thanks Shreyas for pointing this out.

[Tyler Josephson ⚛️]

Thanks Kevin! This is a more appropriate place for questions and discussion. For those curious, here’s the schedule: https://docs.google.com/spreadsheets/d/1ATL-RngI3IGM6uM1ZkXxQdZzYLOAxSn5ZN0MBrfq--o/edit

[Notification Bot]

fnaufel has marked this topic as resolved.

[Notification Bot]

Kevin Buzzard has marked this topic as unresolved.

[Tyler Josephson ⚛️]

My tweet kinda went viral and I have ... 311 people registered for Lean for Scientists and Engineers - 13 in person, 88 only wanting to check out the recording, and 210 indicating interest in joining the online class (so far!). If even half show up on  Tue, Jul 9, 2024, 1:00 PM, that's >100 people.

[Tyler Josephson ⚛️]

About 1/3 undergrads, 1/3 grad students, and 1/3 are folks working outside academia.

25% in engineering, 13% in physical science, 57% in computer science, 31% in mathematics, and 15% in scientific computing.

11% said they're "new to coding altogether," 9% said "I'm comfortable writing scripts," 22% said "I'm comfortable writing functions," and 58% said "I've contributed to a collaborative software project" (I think most of the CS folks are in this category).

Only 32% have taken a course in logic/proofs before

24% never heard of Lean until now, and 41% hear about Lean and wanted to learn, but haven't tried it yet. 20% tried it once or twice and 13% have basic skills in either programming or proofs.

Fun to see lots of interest from newcomers (that was the goal, after all).

[Tyler Josephson ⚛️]

@Kevin Buzzard Bringing this under #Natural sciences is great, but can we actually get a brand-new channel for the course? How can I create a new one, LfSE 2024?

[Kevin Buzzard]

Yeah I can make that (and maybe you can too, just click + by CHANNELS or google for how to do it). The main question you want to decide before you embark on this is whether you want the channel to be public (like this one), public-but-not-on-the-web (i.e. you have to create an account to see the content, this is channels prefixed with a # in the list of channels) or private (you have to create an account and be invited to the channel to see the content, this is channels prefixed with a padlock)

[Tyler Josephson ⚛️]

Ahh, I figured out why I never saw that option - I don't have permission "Note: You will only see the Create channel button if you have permission to create channels."

I want this to be public-but-not-on-the-web.

[Kevin Buzzard]

OK I've created it -- nobody is subscribed to it by default, but you should be able to find it in the list of channels now. #Lean for Scientists and Engineers 2024

[Kim Morrison]

(Note that we recently switch most of our "public-but-not-on-the-web" channels to "public". It's still up to you.)

[Kim Morrison]

I think that @Kevin Buzzard may have skipped a step here, however! We need to know that every channel is either regularly read by a maintainer, or someone who we trust understands the Code of conduct and who is explicitly delegated to loop in the Code of Conduct team whenever necessary on that channel.

[Kim Morrison]

@Tyler Josephson ⚛️, would you mind DM'ing whatever subset of the maintainers you like (e.g. just me and Kevin?) regarding this?

[Tyler Josephson ⚛️]

@Kim Morrison Thanks for the note. I was leaning toward this designation so novices might feel more comfortable asking "dumb" questions without worrying that their chat history would be web-searchable, but still making the channel open so I don't have to manage adding accounts en masse.

And yes! I'd definitely appreciate having a designated maintainer for advising on and enforcing the Code of conduct. We'll likely draw new folks in, and I wouldn't want to fight trolls on my own.

[Kevin Buzzard]

I'll be watching. Kim, let me know if this isn't good enough. I was not aware of this extra step.

[Eric Wieser]

might feel more comfortable asking "dumb" questions without worrying that their chat history would be web-searchable,

Currently nothing on Zulip is web-searchable

[Tyler Josephson ⚛️]

Eric Wieser said:

might feel more comfortable asking "dumb" questions without worrying that their chat history would be web-searchable,

Currently nothing on Zulip is web-searchable

Hmm, I misunderstood. I thought I remembered seeing Zulip chat history archive on Google before. What's the difference between the designations, again?

[Eric Wieser]

• Web public: visible to anyone visiting the Zulip, even those without a login. One day may be google-indexable directly, but not for the near future.
• Public: visible to anyone who visits the Zulip and registers their email (or github, etc). Currently everything under this setting or the setting above is used to populate the archive.
• Private: visible only to people on your course (for instance).

[Eric Wieser]

Some other comments:

• There is a Zulip tracking issue somewhere about making web-public zulip-indexable
• The archive is rarely updated these days (it requires manual intervention from me)
• Probably the archive should switch to only looking at web-public streams web-public:* instead of * in the config

[Tyler Josephson ⚛️]

Oh okay, then I'm find with moving that channel to "Web public." Removing a barrier to create and account will help more people access the content.

[Colin Jones ⚛️]

Hi everyone, my name is Colin Jones. I work with the ATOMS Lab and am helping out with the LfSE meetings asynchronously. For questions about course material, Lean 4 installation, or anything regarding LfSE or you want to set up a meeting with me, please feel free to reach out at my email colinjones166@umbc.edu. I am available for meetings typically in the afternoon (after 5 PM) or on the weekends.