Корисні ресурси для Lean

Добірка корисних ресурсів, які допоможуть опанувати Lean


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