Lean Theorem Prover Mathlib
2 months ago
- #Formal mathematics
- #Mathlib
- #Lean theorem prover
- Mathlib 是一个由用户维护的 Lean 定理证明器库，包含编程基础设施、数学理论和策略指令。
- Lean 和 mathlib 的安装指南可在其官网获取，支持 GitHub Codespace 或 Gitpod 工作空间选项。
- Mathlib 文档包含从源文件自动生成的说明、理论覆盖范围及额外的 Lean 文档资源。
- 社区讨论在 Zulip 聊天室进行，欢迎所有专业水平的用户参与。
- 贡献 mathlib 需遵循风格指南、命名规范和文档标准要求。
- 预编译文件可通过 `lake exe cache get` 获取，构建 mathlib 使用 `lake build` 命令。
- Lean 3 用户迁移至 Lean 4 时，可参考生存指南和使用 `mathport` 的说明文档。
- 依赖项更新使用 `lake update` 命令，文档相关依赖有特定管理规范。
- 提供 mathlib 维护者名单及其专业领域，涵盖数学与技术多个方向。