Zulip Chat Archive

Stream: new members

Topic: Volume!


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Aug 04 2020 at 23:31):

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

view this post on Zulip Jacques Carette (Aug 04 2020 at 23:31):

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

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 04 2020 at 23:57):

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

view this post on Zulip Jacques Carette (Aug 05 2020 at 00:06):

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

view this post on Zulip Jeremy Avigad (Aug 05 2020 at 00:19):

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

view this post on Zulip 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