Stream: new members
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.
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.)
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.)
Mario Carneiro (Aug 18 2020 at 17:25):
You might be interested in the #Program verification stream
Johan Commelin (Aug 18 2020 at 17:26):
Wrenna Robson (Aug 18 2020 at 17:26):
Oh, awesome, thank you.
Wrenna Robson (Aug 19 2020 at 00:55):
(Whoosh! That's the Natural Number Game completed. What a wonderful resource.)
Jalex Stark (Aug 19 2020 at 01:14):
this funky chat interface is actually a pretty amazing tool for organizing a research community.
Wrenna Robson (Aug 19 2020 at 01:15):
Yes, I didn't mean to disparage it! Indeed, I can already see the advantages.
Jalex Stark (Aug 19 2020 at 01:15):
likewise, I didn't mean to accuse you of disparagement :smile:
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...
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.)
Wrenna Robson (Aug 19 2020 at 01:20):
Ah, thank you! Will I find that easily by googling?
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.
Wrenna Robson (Aug 19 2020 at 01:26):
Last updated: May 08 2021 at 10:12 UTC