leanprover-community/mathlib4

# mathlib4  [](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16) [](https://leanprover.zulipchat.com) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) [Mathlib](https://leanprover-community.github.io) 是一个由用户维护的、用于 [Lean 定理证明器](https://leanprover.github.io)的库。 它既包含编程基础设施和数学内容， 也包含使用前者并允许开发后者的 tactic。 ## 安装说明 你可以在[我们的网站](https://leanprover-community.github.io/get_started.html)上找到安装 Lean、mathlib 和辅助工具的详细说明。 或者，点击下方按钮即可打开一个包含该项目的 GitHub Codespace 或 Gitpod 工作区。 [](https://codespaces.new/leanprover-community/mathlib4) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) ## 将 `mathlib4` 作为依赖项使用 请参考 [https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency) ## 试验 一切都安装好了吗？何不从[教程项目](https://leanprover-community.github.io/install/project.html)开始呢？ 如需更多指引，请参阅[学习 Lean](https://leanprover-community.github.io/learn.html)。 ## 文档 除了上面的安装指南和 [Lean 的常规 文档](https://docs.lean-lang.org/lean4/doc/)外，mathlib 的文档还包括： - [mathlib4 文档](https://leanprover-community.github.io/mathlib4_docs/index.html)：从 `.lean` 源文件[自动 生成](https://github.com/leanprover/doc-gen4)的文档。 - 对[目前涵盖的理论](https://leanprover-community.github.io/theories.html)的描述， 以及面向数学家的[概述](https://leanprover-community.github.io/mathlib-overview.html)。 - 一些不特定于 mathlib 的[额外 Lean 文档](https://leanprover-community.github.io/learn.html)（参见“杂项主题”） - 面向希望[为 mathlib 做贡献](https://leanprover-community.github.io/contribute/index.html)的人的文档 许多围绕 mathlib 的讨论都在 [Zulip 聊天 室](https://leanprover.zulipchat.com/)中进行，欢迎你加入，或者不注册直接 旁听。我们欢迎各个专业水平的用户提问！我们还提供了一个[公开讨论 存档](https://leanprover-community.github.io/archive/)，以便于 快速参考。 ### 指南 Mathlib 有以下必须遵守的指南和约定： - [风格指南](https://leanprover-community.github.io/contribute/style.html) - 关于[命名约定](https://leanprover-community.github.io/contribute/naming.html)的指南 - [文档风格](https://leanprover-community.github.io/contribute/doc.html) ### 下载缓存的构建文件 你可以运行 `lake exe cache get` 来下载由 `mathlib4` 的自动化工作流计算的缓存构建文件。 如果遇到莫名其妙的错误， 在再次尝试 `lake exe cache get` 之前，你可以尝试运行 `lake clean` 或 `rm -rf .lake`。 在某些情况下，你可能会尝试使用 `lake exe cache get!` 即使本地已有缓存，它也会重新下载构建文件。 调用 `lake exe cache` 可以查看其帮助菜单。 ### 构建 HTML 文档 [mathlib4_docs 仓库](https://github.com/leanprover-community/mathlib4_docs) 负责生成和发布 [mathlib4 文档](https://leanprover-community.github.io/mathlib4_docs/index.html)。 该仓库可用于在本地构建文档： ``` git clone https://github.com/leanprover-community/mathlib4_docs.git cd mathlib4_docs cp ../mathlib4/lean-toolchain . lake exe cache get lake build Mathlib:docs ``` 最后一步可能需要一些时间（>20 分钟）。 随后可以在 `.lake/build/doc` 中找到 HTML 文件。 ## 从 Lean 3 迁移 对于熟悉 Lean 3 并希望快速掌握 Lean 4 及迁移现有 Lean 3 代码的用户，我们提供： - 面向 Lean 3 用户的[生存指南](https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users) - 在 mathlib 以外的项目上运行 `mathport` 的[说明](https://github.com/leanprover-community/mathport#running-on-a-project-other-than-mathlib)。 `mathport` 是社区用来将整个 `mathlib` 从 Lean 3 移植到 Lean 4 的工具。 ### 依赖项 如果你是 mathlib 的贡献者并希望更新依赖项，请使用 `lake update`， 或使用 `lake update batteries aesop`（或类似命令）来更新部分依赖项。 这将正确更新 `lake-manifest.json` 文件。 在提交对此文件的更改后，你需要创建一个 PR。 请不要再像以前建议的那样运行 `lake update -Kdoc=on`，因为与文档相关的 依赖项应仅在 CI 构建文档时包含。 ## 维护者： 包含更详细信息的列表，请参阅 https://leanprover-community.github.io/teams/maintainers.html * Anne Baanen (@Vierkantor): algebra, number theory, tactics * Matthew Robert Ballard (@mattrobball): algebra, algebraic geometry, category theory * Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory * Kevin Buzzard (@kbuzzard): algebra, number theory, algebraic geometry, category theory * Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering * Bryan Gin-ge Chen (@bryangingechen): documentation, infrastructure * Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry * Anatole Dedecker (@ADedecker): topology, functional analysis, calculus * Rémy Degenne (@RemyDegenne): probability, measure theory, analysis * Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics * Frédéric Dupuis (@dupuisf): linear algebra, functional analysis * Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory * Markus Himmel (@TwoFX): category theory * Yury G. Kudryashov (@urkud): analysis, topology, measure theory * Robert Y. Lewis (@robertylewis): tactics, documentation * Jireh Loreaux (@j-loreaux): analysis, topology, operator algebras * Heather Macbeth (@hrmacbeth): geometry, analysis * Patrick Massot (@patrickmassot): documentation, topology, geometry * Bhavik Mehta (@b-mehta): category theory, combinatorics * Kyle Miller (@kmill): combinatorics, tactics, metaprogramming * Kim Morrison (@kim-em): category theory, tactics * Oliver Nash (@ocfnash): algebra, geometry, topology * Filippo A. E. Nuccio (@faenuccio): algebra, functional analysis, homology, number theory * Joël Riou (@joelriou): category theory, homology, algebraic geometry * Michael Rothgang (@grunweg): differential geometry, analysis, topology, linters * Damiano Testa (@adomani): algebra, algebraic geometry, number theory, tactics, linters * Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry * Eric Wieser (@eric-wieser): algebra, infrastructure ## 前任维护者： * Jeremy Avigad (@avigad): analysis * Reid Barton (@rwbarton): category theory, topology * Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages * Johannes Hölzl (@johoelzl): measure theory, topology * Simon Hudon (@cipher1024): tactics * Chris Hughes (@ChrisHughes24): algebra

标签：Lean 4, 函数式编程, 定理证明, 形式化验证, 数学库