New member

Stream: new members

[Andre]

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]

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]

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]

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?

Thank you in advance!

[Bryan Gin-ge Chen]

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]

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

Specifically undergraduate math that's in mathlib https://leanprover-community.github.io/undergrad.html and what's not in mathlib https://leanprover-community.github.io/undergrad_todo.html

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

[Yaël Dillies]

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

[Kyle Miller]

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]

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]

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]

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]

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

Thanks! I'll start with this as soon as I can.

Kyle Miller said:

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

Specifically undergraduate math that's in mathlib https://leanprover-community.github.io/undergrad.html and what's not in mathlib https://leanprover-community.github.io/undergrad_todo.html

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

Thank you!

[Scott Morrison]

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]

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]

No infinity categories yet, of any variety.

[Kevin Buzzard]

@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]

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]

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]

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

[Adam Topaz]

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

[Scott Morrison]

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]

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]

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

[Hanno Becker]

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]

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

[Eric Wieser]

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]

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

[Johan Commelin]

Adam Topaz said:

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]

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]

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