## Stream: new members

### Topic: New member

#### Andre (Nov 04 2021 at 18:45):

Hi Everyone,

I'm slowly getting familiar with Zulip/Lean. I want to learn more math so it could help me abstract complex programming problems so it'll be easier to reason about them and synthesis solutions and understanding. Is this the right place?

The last math education was Calc 3 in Community College which I failed. I really want to understand Category theory. I feel the web and it's interactions are so complex that I feel a constant need to find a new language to simplify all the complex ideas that programmers have to deal with.

Any ideas on where a person like me can start?

I'm curious about dependent type theory and Category theory.

#### Horatiu Cheval (Nov 04 2021 at 18:58):

For category theory, if you are first and foremost a programmer, there is always the classical by now book by Bartosz Milewski: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

#### Kyle Miller (Nov 04 2021 at 18:58):

I've been hearing a buzz about applied category theory recently. I haven't read it, but I've paged through 7 sketches in compositionality: an invitation to applied category theory. If you don't have some abstract algebra background, I imagine it would be tough going without guidance, but at the least it looks like it might give you some idea of what the subject is about.

#### Lorenzo Riva (Nov 04 2021 at 19:33):

Hi everyone,

Following Jeremy Avigad's advice from today's Topos Institute Colloquium talk I'd like to introduce myself and ask a couple of basic questions regarding how to better learn Lean. I'm a graduate student at Notre Dame currently interested in factorization homology and category theory. I have a fairly strong background in topology and category theory so I think I might be well-equipped to formalize those two areas, if that hasn't been done already.

So my first question is: what is the best resource to learn the fundamentals of Lean, dependent type theory, and formalization?
My second question (from which I will benefit only in the future) is: once I'm sufficiently fluent in Lean, where can I find a list of things that need to be formalized?

#### Bryan Gin-ge Chen (Nov 04 2021 at 19:34):

Welcome Lorenzo! We've got a page with learning resources for Lean 3 here, which is hopefully a good starting point: https://leanprover-community.github.io/learn.html

#### Kyle Miller (Nov 04 2021 at 19:35):

A curated list of what's in mathlib https://leanprover-community.github.io/mathlib-overview.html

The mathlib docs: https://leanprover-community.github.io/mathlib_docs/

#### Yaël Dillies (Nov 04 2021 at 19:36):

About your second question, there's plenty to do! What area are you interested in?

#### Kyle Miller (Nov 04 2021 at 19:40):

A solid approach, too, is to formalize something that interests you, whether or not it's already in mathlib, and along the way you'll start finding missing lemmas that might be generally useful, and after some polishing they can be your first contributions. Mathlib is pretty big, so that can help with getting a feel for what's in it, too.

#### Kyle Miller (Nov 04 2021 at 19:47):

I guess one of my first contributions was the trivial statement #3391 (how have there been almost 7000 PRs since then??) and it was from some discussion about how to make proofs involving nested quantifiers nicer.

#### Andre (Nov 04 2021 at 20:05):

Kyle Miller said:

I've been hearing a buzz about applied category theory recently. I haven't read it, but I've paged through 7 sketches in compositionality: an invitation to applied category theory. If you don't have some abstract algebra background, I imagine it would be tough going without guidance, but at the least it looks like it might give you some idea of what the subject is about.

Thank you! I don't have an abstract algebra background and it is kinda tough going in so far without guidance. However, I have a strange feeling pushing me to continue.

#### Yaël Dillies (Nov 04 2021 at 20:28):

Kyle Miller said:

I guess one of my first contributions was the trivial statement #3391 (how have there been almost 7000 PRs since then??) and it was from some discussion about how to make proofs involving nested quantifiers nicer.

I know!! I started in MArch and the number of PR is already close to doubling.

#### Lorenzo Riva (Nov 05 2021 at 02:57):

Bryan Gin-ge Chen said:

Welcome Lorenzo! We've got a page with learning resources for Lean 3 here, which is hopefully a good starting point: https://leanprover-community.github.io/learn.html

Kyle Miller said:

A curated list of what's in mathlib https://leanprover-community.github.io/mathlib-overview.html

The mathlib docs: https://leanprover-community.github.io/mathlib_docs/

Thank you!

#### Scott Morrison (Nov 06 2021 at 22:36):

Yay factorization homology! Welcome.

Unfortunately we don't have a particularly good "todo list" for formalisation, and it can take some experimentation / asking around to identifying the boundary of what is currently possible. Throwing out ideas here on zulip generally gets fast feedback.

#### Scott Morrison (Nov 06 2021 at 22:38):

A lot of the category theory library has been built with the beginnings of algebraic geometry (spec / gamma) or the beginning of homological algebra in mind.

#### Scott Morrison (Nov 06 2021 at 22:38):

No infinity categories yet, of any variety.

#### Kevin Buzzard (Nov 06 2021 at 22:57):

@Lorenzo Riva blowing my own trumpet, but here is a course I gave to math PhD students about undergraduate mathematics in Lean, and here is the course I taught this term as part of the "intro to proof" course at Imperial. These resources get you straight in to the mathematics without bothering too much about the type theory story.

#### Lorenzo Riva (Nov 07 2021 at 00:53):

Kevin Buzzard said:

Lorenzo Riva blowing my own trumpet, but here is a course I gave to math PhD students about undergraduate mathematics in Lean, and here is the course I taught this term as part of the "intro to proof" course at Imperial. These resources get you straight in to the mathematics without bothering too much about the type theory story.

Thank you! I started with the two interactive textbooks mentioned on the website but I'll definitely take a look at your material.

#### Lorenzo Riva (Nov 07 2021 at 00:54):

Scott Morrison said:

No infinity categories yet, of any variety.

What about simplicial sets? That might be one of the directions I can take and then transition to infinity-categories

#### Adam Topaz (Nov 07 2021 at 01:13):

We have simplicial sets (and simplicial objects in general) around algebraic_topology/simplicial e.g. docs#sSet

#### Adam Topaz (Nov 07 2021 at 01:20):

Unfortunately, we don't yet have simplicial homotopy, but it should be a very doable project!

#### Scott Morrison (Nov 07 2021 at 01:52):

Simplifical stuff working towards e.g. Rezk's notes on quasicategories would be a great project for someone who knows this stuff. The mathlib prerequisites are hopefully mostly in place??

#### Hanno Becker (Nov 07 2021 at 06:22):

Ahoi! I'm Hanno, a former PhD student from Bonn (application of homotopical algebra to knot theory), did some formal verification in Coq for a security company afterwards, and these days I'm working on post-quantum cryptography at Arm Research in Cambridge, UK.
I joined because out of curiosity about the development of Lean and the "news" about the liquid tensor experiment :-)

#### Yaël Dillies (Nov 07 2021 at 07:18):

Hey! We're meeting every Wednesday in the CMS from 3 to 6pm, if you wanna join!

#### Hanno Becker (Nov 08 2021 at 06:41):

Yaël Dillies said:

Hey! We're meeting every Wednesday in the CMS from 3 to 6pm, if you wanna join!

Thanks Yaël! Is that a general meeting about Lean, or specific to liquid tensor / any other project?

#### Johan Commelin (Nov 08 2021 at 06:43):

@Hanno Becker I've never been to these meetings. But I think they are Lean-generic

#### Eric Wieser (Nov 08 2021 at 06:44):

Yes, it's pretty much an excuse to hang out with other Lean users in person (with laptops), from my sample of 1.

#### Eric Wieser (Nov 08 2021 at 06:45):

Sometimes mathlib maintainers are persuaded to come along so that they can be haggled about reviewing PRs.

#### Johan Commelin (Nov 08 2021 at 08:19):

Unfortunately, we don't yet have simplicial homotopy, but it should be a very doable project!

@Lorenzo Riva Note that simplicial homology (two letters differ :wink:) is basically done in the liquid tensor experiment. Just pointing this out to avoid duplication.

#### Yaël Dillies (Nov 08 2021 at 08:33):

Eric Wieser said:

Sometimes mathlib maintainers are persuaded to come along so that they can be haggled about reviewing PRs.

again with a sample size of one :grinning_face_with_smiling_eyes:

#### Yaël Dillies (Nov 08 2021 at 08:34):

I assume you will be coming this week, Eric, right??

Last updated: Dec 20 2023 at 11:08 UTC