Mathlib

Mathlib是面向定理证明器Lean的开源数学库，由数学家和开发者社区共同开发，收录了代数、分析、拓扑、数论等多个领域的定义和定理，并以Lean可检查的形式化证明写成。

由于它让人在编写形式化证明时可以复用已经验证的定义和定理，因此被广泛用于数学形式化和基于AI的定理证明研究。

本条目依据AIPOST的文章与广为人知的事实整理。如有错误，请通过更正请求告诉我们。