HackerPapers

arXiv:2108.00484cs.LO

Elements of Differential Geometry in Lean: A Report for Mathematicians

Anthony Bordg, Nicolò Cavalleri

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

Abstract

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.

arXiv comments
To appear in the proceedings of the Fifth Workshop on Formal Mathematics for Mathematicians (part of CICM 2021)
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science math.DGDifferential Geometry

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Aug 2021 to Aug 2021. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.