Guidance on Formalizing Probability Theory and Request for Tutorials

[zhimi64]

Hi,

First of all, thank you for all the great work on Lean! I'm new to Lean and find it both fascinating and quite complex.

I'm currently trying to formalize some propositions related to probability theory, but I'm struggling to get started. Do I need to have a solid understanding of measure theory before I can effectively work with probability theory in Lean? I noticed that the Mathematics in Lean book does not have a chapter on probability theory. Is there a plan to add a tutorial or section on probability theory in the future?

Any guidance or resources you could point me to would be greatly appreciated.

Thanks!

[avigad]

We don't have immediate plans to add a chapter on probability theory, but it would definitely be good to have one, and hopefully we will get to it eventually. In the meantime, Rémy Degenne has just written a helpful blog post: https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/. Also, the Lean Zulip chat is a good place to ask questions.