Создание математической библиотеки будущего
Небольшое сообщество математиков использует программу Lean для создания новой цифровой базы. Они надеются, что она обеспечит будущее их научной области. Ежедневно десятки математиков-единомышленников встречаются в чате Zulip, чтобы работать, как они считают, над созданием будущего их научной области. Все они – поклонники программы Lean. Это инструмент интерактивного доказательства теорем, который, в принципе, способен помогать математикам...