25 citations · 45 across the 10 of their papers we have counts for
Showing 2021Show all
2 papers · 1 filter
cs.LO2021
Elements of Differential Geometry in Lean: A Report for Mathematicians
Anthony Bordg, Nicolò Cavalleri
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,…
math.AG2021★ 12 cited
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
Anthony Bordg, Lawrence Paulson, Wenda Li
Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setti…