Stream: Announcements

Topic: The Whitehead Theorem and The Puppe Sequence

Dean Young (Nov 21 2023 at 00:30):

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.

Later plans will extend these features to Isabelle, perhaps helping to bridge the conceptual divide between proof assistants based in types vs. higher order logic.

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.

Last updated: Dec 22 2024 at 08:21 UTC