2 papers
math.DG2024
Complete non-compact -manifolds from -bundles over AC Calabi Yau manifolds
Nicolò Cavalleri
We develop a new construction of complete non-compact 8-manifolds with Riemannian holonomy equal to . As a consequence of the holonomy reduction, these mani…
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,…