5
[2108.00484] Elements of Differential Geometry in Lean: A Report for Mathematici...
source link: https://arxiv.org/abs/2108.00484
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
[Submitted on 1 Aug 2021]
Elements of Differential Geometry in Lean: A Report for Mathematicians
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.
Comments:
To appear in the proceedings of the Fifth Workshop on Formal Mathematics for Mathematicians (part of CICM 2021)
Subjects:
Logic in Computer Science (cs.LO); Differential Geometry (math.DG)
MSC classes:
03B35, 53-04
Cite as:
arXiv:2108.00484 [cs.LO]
(or
arXiv:2108.00484v1 [cs.LO] for this version)
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK