We would like to announce our (open source and publicly available)
library for working with general probability spaces in Coq. Starting
with Sigma-Algebras, it works its way up to general expectation, and
general conditional expectation (defined over any nonnegative or
finite expectation measurable random variable), with the expected
This is used for various applications, such as our proof of
Dvoretzky’s convergence theorem for stochastic processes. A preprint
discussing this work is available at [2202.05959] Formalization of a Stochastic Approximation Theorem,
and includes a description of how the library is built up.
We have also been working on developing some martingale theory, and
recently formalized the martingale convergence theorem and the
optional stopping time theorem. To our knowledge, this is the first
mechanization (in Coq) of the latter theorem
(It is still marked as unclaimed on Formalizing 100 Theorems).
Generated documentation on this result is available at
The library is available at GitHub - IBM/FormalML: Formalization of Machine Learning Theory with Applications to Program Synthesis
We welcome users and collaborators, and would love to develop a
community of users interested in this space.
For questions and discussions about potential collaborations, please
contact Avi at firstname.lastname@example.org, or via zulip.
- The FormalML team (Avi, Barry, and Koundinya)