{"id":"arxiv:2108.00484","kind":"preprint","title":"Elements of Differential Geometry in Lean: A Report for Mathematicians","authors":["Anthony Bordg","Nicolò Cavalleri"],"author_count":2,"year":2021,"published":"2021-08-01","venue":null,"cited_by":null,"doi":null,"arxiv_id":"2108.00484","nct_id":null,"source_url":"https://arxiv.org/abs/2108.00484","archive_url":"https://space-kitty.com/papers/arxiv:2108.00484","updated":"2021-08-01","pmid":null,"pmcid":null,"openalex_id":null,"pdf_url":"https://arxiv.org/pdf/2108.00484","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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO","math.DG"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[],"cited_in_dossiers":[]}