onboarding

Stream: new members

[Welcome Bot]

A #new members stream is great for onboarding new members.

If you're reading this and aren't the first person here, introduce yourself in a new thread using your name as the topic! Type c or click on New Topic at the bottom of the screen to start a new topic.

[Wrenna Robson]

Hey...? This is a fairly funky chat interface.

The welcome bot thing said to introduce myself, but everyone seems in the middle of large discussions. I'm going to do it anyway, though. Hi. I'm Wrenna. I just finished the "Power World" series on https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/. I... this Lean thing seems like the coolest thing I have literally ever seen? Like the notion that this is, basically, the future, feels so right. So I decided to join this and maybe keep track of it and learn it a bit (though it really isn't the stuff I'm meant to be doing... related, but not on target. Very fun though.)

[Wrenna Robson]

(I'm a PhD student over at RHUL's Cyber Security CDT: I'm just finishing writing up - more accurately procrastinating finishing writing up - my first year summer project using Cryptol (domain-specific formal specification language), which is sort of how I started reading about Lean, though I was already tangentially aware of it. I've a maths background, though, originally.)

[Mario Carneiro]

You might be interested in the #Program verification stream

[Johan Commelin]

Welcome!

[Wrenna Robson]

Oh, awesome, thank you.

[Wrenna Robson]

(Whoosh! That's the Natural Number Game completed. What a wonderful resource.)

[Jalex Stark]

this funky chat interface is actually a pretty amazing tool for organizing a research community.

[Wrenna Robson]

Yes, I didn't mean to disparage it! Indeed, I can already see the advantages.

[Jalex Stark]

likewise, I didn't mean to accuse you of disparagement :smile:

[Wrenna Robson]

My next task is getting my head round actually installing Lean and playing with stuff outside the fairly gentle NNG sandbox...

[Scott Morrison]

There are a whole lot of tutorials and exercises from the recent "Lean for the Curious Mathematician" workshop. (Also videos of the lectures.)

[Wrenna Robson]

Ah, thank you! Will I find that easily by googling?

[Alex J. Best]

The main site is https://leanprover-community.github.io/ and #install should have instructions, https://www.youtube.com/watch?v=T4yt53dCqCU&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv is the playlist of install / overview videos.

[Wrenna Robson]

Ta.