Related papers: Synthetic Differential Geometry in Lean
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, but eager to learn more about the formalization of…
This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on…
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 developments in linear algebra, analysis, measure theory and…
We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic objects which encode infinitesimal symmetries, and as such…
We try to convince the reader that the categorical version of differential geometry, called Synthetic Differential Geometry (SDG), offers valuable tools which can be applied to work with some unsolved problems of general relativity. We do…
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…
The continuous functional calculus is perhaps the most fundamental construction in the theory of operator algebras, especially $C^{*}$-algebras. Here we document our formalization of the continuous functional calculus in Lean, which…
Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean's Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none…
Some differential equations are considered in the context of Synthetic Differential Geometry. Here, this means that not only nilpotent infinitesimals, but also the formation of function spaces, is exploited. In particular, we utilize…
We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One goal of the mathlib project is to contain all of the topics of…
Synthetic algebraic geometry uses homotopy type theory extended with three axioms to develop algebraic geometry internal to a higher version of the Zariski topos. In this article we make no essential use of the higher structure and use…
Chemical theory can be made more rigorous using the Lean theorem prover, an interactive theorem prover for complex mathematics. We formalize the Langmuir and BET theories of adsorption, making each scientific premise clear and every step of…
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have…
Weil prolongations of a Lie group are naturally Lie groups. It is not known in the theory of infinite-dimensional Lie groups how to construct a Lie group with a given Lie algebra as its Lie algebra or whether there exists such a Lie group…
The ongoing development of Lean 4's Mathlib has produced a macroscopic structural complexity that interweaves logical, mathematical, and infrastructural dependencies. We present a network analysis of this library, extracting its dependency…
Groupoids provide a more appropriate framework for differential geometry than principal bundles. Synthetic differential geometry is the avant-garde branch of differential geometry, in which nilpotent infinitesimals are available in…
The central object of synthetic differential geometry is microlinear spaces. In our previous paper [Microlinearity in Frolicher spaces -beyond the regnant philosophy of manifolds-, International Journal of Pure and Applied Mathematics, 60…
The thesis presents the subject of synthetic topology, especially with relation to metric spaces. A model of synthetic topology is a categorical model in which objects possess an intrinsic topology in a suitable sense, and all morphisms are…
This paper gives a first step towards developing synthetic differential geometry within homotopy type theory. Its model theory will be discussed in a subsequent paper.
Integration is the final key step when turning an infinitesimal argument into a result applicable to quantities of finite size. Conceptually, it is about combining infinitesimal contributions to a finite whole. We make a first step towards…