Freek 62 + FormalML

Stream: general

[Koundinya Vajjha]

(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]

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]

cc @Jason KY.

[Koundinya Vajjha]

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

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