Higher order differential calculus in mathlib
Logic in Computer Science
2025-09-08 v1
Abstract
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 ways from standard textbook definitions: we allow arbitrary fields of scalars, we work with functions defined on domains rather than full spaces, and we integrate analytic functions in the broader scale of smooth functions. These generalizations introduce significant challenges, which we address from both the mathematical and the formalization perspectives.
Keywords
Cite
@article{arxiv.2509.04922,
title = {Higher order differential calculus in mathlib},
author = {Sébastien Gouëzel},
journal= {arXiv preprint arXiv:2509.04922},
year = {2025}
}