80 citations · 87 across the 7 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2025
Higher order differential calculus in mathlib
Sébastien Gouëzel
We report on the higher-order differential calculus library developed inside the Lean mathematical library mathlib. To support a broad range of applications, we depart in several w…
cs.LO2022★ 1 cited
A formalization of the change of variables formula for integrals in mathlib
Sébastien Gouëzel
We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on devel…
cs.LO2021
Formalizing the Gromov-Hausdorff space
Sébastien Gouëzel
The Gromov-Hausdorff space is usually defined in textbooks as "the space of all compact metric spaces up to isometry". We describe a formalization of this notion in the Lean proof…