search

avigad / mathematics_in_lean_source

Source code for the Mathematics in Lean tutorial.
89 stars 70 forks source link

Guidance on Formalizing Probability Theory and Request for Tutorials #248

Open zhimi64 opened 1 month ago

zhimi64 commented 1 month ago

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 commented 4 weeks ago

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.