You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Dean Young (Nov 21 2023 at 00:22):Linear Library Phase I (December 2023-August 2024)
Hi all,
I am Dean, a graduate student in mathematics at New York University. This bulletin is for everyone interested in computerized mathematics and categories, such as the mathematics in Mathlib 4.
The linearlibrary team is interested in enlisting the help of students and mathematicians interested in homotopy and simplicial sets to prove twenty-four important results in homotopy theory and stable homotopy theory inside the Lean 4 computer proof assistant. Powerful yet convenient, these results will largely be established for Mathlib 4's pre-existing objects, such as those involving simplicial sets.
Are you interested in the twelve theorems outlined in the document here? Reach out to ``edeany@nyu.edu" with the subject "Whitehead Theorem and Puppe Sequence for Lean 4" for more information, or if you would like to participate.