论文标题
维护正式数学库
Maintaining a Library of Formal Mathematics
论文作者
论文摘要
精益数学库Mathlib是由一个具有不同背景和经验水平的用户社区开发的。为了降低贡献者的入境障碍并减轻审查贡献的负担，我们为图书馆开发了许多工具，这些工具会检查证明代码中的细微错误的证明开发，并生成适合我们各种受众的文档。
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.
