Stream: new members

Topic: Volume!

Jacques Carette (Aug 04 2020 at 23:23):

New member here. Wanted to lurk for a while, see how things are done, learn stuff.

But the volume of posts is quite daunting. Several hundred per day. Wow. Very intimidating!

Dan Stanescu (Aug 04 2020 at 23:25):

Bienvenue, Jacques! I don't think you should worry about that too much. Start by trying to formalize things on your own and ask questions when you get stuck.

Jacques Carette (Aug 04 2020 at 23:29):

I guess I should introduce myself too: I'm not new to formalization at all. I'm author of stuff that's in the Agda stdlib, and about 1/2 of the agda-categories library. I'm also co-author of a branch of HOL Light, HOL Light QE, that adds quote and eval to HOL Light. Before that, and a long time ago, I worked at Maplesoft (makers of Maple) for 11 years. I was head of the Math Group for quite a few of those years, so I'm kind of a symbolic computation expert. And Chair of IFIP WG 2.11 on metaprogramming, so I guess I'm an expert at that too. But a total novice at Lean.

Dan Stanescu (Aug 04 2020 at 23:31):

Oh, it sounds like you have no reason to ever get stuck at all.

Jacques Carette (Aug 04 2020 at 23:31):

It's formalization! I, like everyone else, gets stuck all the time.

Scott Morrison (Aug 04 2020 at 23:38):

Welcome, Jacques! Great to see you here. :-)

The threading on zulip is really nice, so it's usually straightforward to ignore the conversations you don't have time for.

Scott Morrison (Aug 04 2020 at 23:40):

We'd love to hear your impressions, criticisms (or patches and PRs!) on any aspect of Lean or mathlib --- it's incredibly useful to have expert eyes from other theorem provers. (Unsurprisingly you'll find us already too set in our ways in some places, but we want to learn!)

Jacques Carette (Aug 04 2020 at 23:41):

I'm on this zulip and the category theory one, 5 slack channels and 5 on discord too. And then there's email and twitter (PL twitter is amazing). Information overload.

Jacques Carette (Aug 04 2020 at 23:42):

I'm going to soak it all in a bit longer before I jump in and criticize.

Scott Morrison (Aug 04 2020 at 23:43):

If you need pointers to documentation, where to find particular developments, etc. just ask. If you ever want a tour of the categories library, just ping me, as I'd love to hear your take comparing to how things are done in agda (which I don't know at all well).

Jacques Carette (Aug 04 2020 at 23:44):

But I can meta-comment: I'm unlikely to 'criticize' Lean, the system, very much. Though I might point out features of other systems to consider. mathlib, that's a very different kettle of fish! There, I have actual expertize, and will jump in when I think that my 'contribution' can make an actual difference. [I'm going to try really hard to not criticize when it's tilting at windmills. I do that enough as it is.]

Jacques Carette (Aug 04 2020 at 23:45):

Getting a tour of the category library would be nice. Not right now, but perhaps in the next couple of weeks.

Jalex Stark (Aug 04 2020 at 23:45):

in addition to scott's offer to tour the category theory library, scott has written a wonderful set of exercises to introduce it, available at leanproject get lftcm2020, along with several other great sets of exercises

Jacques Carette (Aug 04 2020 at 23:46):

But I am actively exploring parts of the design space (proof relevance, setoids, purely constructive) that I would not necessarily recommend.

Jacques Carette (Aug 04 2020 at 23:47):

I'm having fun doing it that way, and it turns out to work way better than I had any hope to expect. When Jason and I started out, we both expected to learn "the hard way" why that part of the design space was a mistake. We learned the opposite: that it's a happy place to be!

Jacques Carette (Aug 04 2020 at 23:50):

https://arxiv.org/abs/2005.07059 for those who are curious for a write-up for humans. https://agda.github.io/agda-categories/ for those who want to browse what's available.

Scott Morrison (Aug 04 2020 at 23:57):

Thanks for the pointers, I'll take a look!

Jacques Carette (Aug 05 2020 at 00:06):

All comments (and questions) on that are welcome too.

Jeremy Avigad (Aug 05 2020 at 00:19):

Hi, Jacques! It's nice to see you here.

Jacques Carette (Aug 05 2020 at 00:40):

Hi Jeremy. It's fun to hang out in yet another place where I know some neat people hang out and do interesting work.

Last updated: May 11 2021 at 21:10 UTC