实用的 Lean 资源

一系列实用资源，助你精通 Lean

  • 官方网站是关于这门语言内容的主要资源库。站点上有一个在线演练场，你无需安装任何东西就能试用这门语言。
  • Reservoir 收录、构建并测试 Lean 与 Lake 生态系统中的包。想找第三方包，来这里就对了。
  • Lean Community 是围绕 Lean 生态系统的协作式开源社区，负责 mathlib，即 Lean 4 主要的社区驱动数学库。
  • Lean 4 Zulip Chat 是 Lean Community 的主要聊天渠道。