Zulip Chat Archive

Stream: new members

Topic: onboarding


view this post on Zulip Welcome Bot (Feb 26 2018 at 16:02):

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.

view this post on Zulip Wrenna Robson (Aug 18 2020 at 17:15):

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.)

view this post on Zulip Wrenna Robson (Aug 18 2020 at 17:19):

(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.)

view this post on Zulip Mario Carneiro (Aug 18 2020 at 17:25):

You might be interested in the #Program verification stream

view this post on Zulip Johan Commelin (Aug 18 2020 at 17:26):

Welcome!

view this post on Zulip Wrenna Robson (Aug 18 2020 at 17:26):

Oh, awesome, thank you.

view this post on Zulip Wrenna Robson (Aug 19 2020 at 00:55):

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

view this post on Zulip Jalex Stark (Aug 19 2020 at 01:14):

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

view this post on Zulip Wrenna Robson (Aug 19 2020 at 01:15):

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

view this post on Zulip Jalex Stark (Aug 19 2020 at 01:15):

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

view this post on Zulip Wrenna Robson (Aug 19 2020 at 01:18):

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

view this post on Zulip Scott Morrison (Aug 19 2020 at 01:19):

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

view this post on Zulip Wrenna Robson (Aug 19 2020 at 01:20):

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

view this post on Zulip Alex J. Best (Aug 19 2020 at 01:26):

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.

view this post on Zulip Wrenna Robson (Aug 19 2020 at 01:26):

Ta.


Last updated: May 08 2021 at 10:12 UTC