Lean中的微分几何元素：给数学家的报告
Elements of Differential Geometry in Lean: A Report for Mathematicians
摘要：
我们报告我们的经验形式化微分几何与mathlib，精益数学库。我们的叙述是面向几何学家的，他们没有类型论的知识，但渴望了解更多关于数学的形式化，也许好奇到在未来给Lean一个尝试。为了达到这个效果，我们强调可能令人惊讶的形式化和它的笔和纸的对等物之间的差异所产生的精益的平等待遇。我们的三个案例研究是李群，向量丛和李群的李代数。
英文摘要：
We report on our experience formalizing differential geometry with mathlib, the Lean mathematical library. Our account is geared towards geometers with no knowledge of type theory, but eager to learn more about the formalization of mathematics and maybe curious enough to give Lean a try in the future. To this effect, we stress the possibly surprising difference between the formalization and its pen-and-paper counterpart arising from Lean's treatment of equality. Our three case studies are Lie groups, vector bundles and the Lie algebra of a Lie group.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
