Papers With

← All papers
First page of Higher order differential calculus in mathlib

Higher order differential calculus in mathlib

Sébastien Gouëzel

cs.LO Sep 5, 2025 · v1
formalization mathlib analysis
Read PDF arXiv abstract
TL;DR
Reports on the higher-order differential calculus library formalized inside Lean's mathematical library Mathlib.
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.
Problem

Higher-order differential calculus is essential for formalizing analysis and differential geometry, but formalizing it in a proof assistant requires departures from standard textbook definitions to support broad applications.

Approach

The authors develop a higher-order differential calculus library inside Lean's Mathlib. They allow arbitrary fields of scalars, work with functions defined on domains rather than full spaces, and integrate analytic functions in the broader scale of smooth functions. These generalizations introduce challenges addressed from both mathematical and formalization perspectives.

Results

The library is part of Mathlib and supports a broad range of applications. The design choices (domain-based definitions, arbitrary scalar fields, smooth-analytic integration) resolve significant formalization challenges while remaining mathematically general.