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