# Zulip Chat Archive

## Stream: general

### Topic: Freek 62 + FormalML

#### Koundinya Vajjha (Mar 29 2022 at 14:56):

(Cross-posting from the Coq discourse/zulip in case there is interest here):

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

properties.

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 https://arxiv.org/abs/2202.05959,

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 http://www.cs.ru.nl/~freek/100/).

Generated documentation on this result is available here.

The library is available at https://github.com/IBM/FormalML

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 Shinnar .

- The FormalML team (@Avi Shinnar, Barry Trager, and @Koundinya Vajjha )

#### Eric Wieser (Mar 29 2022 at 14:58):

I assume the name clash with https://github.com/google/formal-ml is unintentional, and there is no overlap in the contributors?

#### Yaël Dillies (Mar 29 2022 at 14:58):

cc @Jason KY.

#### Koundinya Vajjha (Mar 29 2022 at 15:02):

Eric Wieser said:

I assume the name clash with https://github.com/google/formal-ml is unintentional, and there is no overlap in the contributors?

Indeed. Both libraries are distinct. `formal-ml`

is Lean and `FormalML`

is entirely in Coq.

#### Jason KY. (Mar 29 2022 at 15:08):

We have the forward direction of the optional stopping theorem for discrete martingales here

Last updated: Dec 20 2023 at 11:08 UTC