實用的 Lean 資源

精選的實用資源,幫助你精通 Lean


  • Lean 官方網站 是這門語言相關內容的主要集散地。 網站上還有個線上遊樂場,讓你不用安裝任何東西就能試試這門語言。
  • Reservoir 會索引、建置並測試 Lean 與 Lake 生態系中的套件。 想找第三方套件,來這裡就對了。
  • Lean 社群 是一個圍繞 Lean 生態系的協作開源網路。 它負責維護 mathlib,也就是 Lean 4 主要的社群數學函式庫。
  • Lean 4 Zulip 聊天室 是 Lean 社群主要的交流聊天室。