Volume!

Stream: new members

[Jacques Carette]

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]

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]

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]

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

[Jacques Carette]

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

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

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]

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]

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

[Jalex Stark]

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]

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

[Jacques Carette]

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]

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]

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

[Jacques Carette]

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

[Jeremy Avigad]

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

[Jacques Carette]

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