Stream: Coq users

Topic: Forty-eight theorems for homotopy in Lean 4


view this post on Zulip Dean Young (Nov 21 2023 at 00:26):

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.

view this post on Zulip Huỳnh Trần Khanh (Nov 21 2023 at 00:40):

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

view this post on Zulip Notification Bot (Nov 21 2023 at 01:31):

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