Zulip Chat Archive

Stream: new members

Topic: category theory

Yono (Jul 20 2023 at 15:12):

hello, I want to do category theory with lean4. What pages helps me?

Notification Bot (Jul 20 2023 at 15:14):

A message was moved here from #general > Paid studies to formalize math problems in Lean by Eric Wieser.

Adam Topaz (Jul 20 2023 at 15:18):

We have an extensive category theory library in mathlib4, all available here: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/CategoryTheory

Adam Topaz (Jul 20 2023 at 15:19):

Kevin Buzzard has ported some category theory exercises to lean4, which were originally written by Scott Morrison in lean3. You can find them here: https://github.com/adamtopaz/CopenhagenMasterclass2023/tree/master/CategoryTheoryExercises

Last updated: Dec 20 2023 at 11:08 UTC