**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.

I don't speak your language but this is patching mathlib right

This topic was moved to #Miscellaneous > Forty-eight theorems for homotopy in Lean 4 by Karl Palmskog.

Last updated: Jun 23 2024 at 04:03 UTC