Корисні ресурси для Lean
Добірка корисних ресурсів, які допоможуть опанувати Lean
-
Офіційний сайт містить головне сховище матеріалів про мову.
Там є онлайн-пісочниця, де можна спробувати мову, нічого не встановлюючи.
-
Reservoir індексує, збирає та тестує пакети в екосистемі Lean і Lake.
Саме тут варто шукати сторонні пакети.
-
Lean Community - це спільна мережа з відкритим кодом навколо екосистеми Lean.
Вона відповідає за mathlib, головну математичну бібліотеку для Lean 4, яку розвиває спільнота.
-
Lean 4 Zulip Chat - головний чат спільноти Lean.