Dear math-comp analysis contributors,

I am a postdoc at IST Austria working in Random Matrix Theory - the study of eigenvalues and eigenvectors of matrices whose entries are random. I discovered Coq recently and I formed the project of formalizing a few classical proofs, beginning with the so-called "Wigner semicircle law", which is considered to be the first important discovery in this area.

To do so, I will certainly need measure theory, linear algebra, complex analysis, and a little bit of combinatorics as well. Advice or suggestions are most welcome!

some pieces of measure theory have been done for MathComp in these projects: https://github.com/jtassarotti/coq-proba https://github.com/affeldt-aist/infotheo

there are more pieces of measure theory in mathcomp-analysis but it is in a PR :-/

some applied probability theory via Infotheo here that may be relevant (but more of a long shot): https://github.com/certichain/ceramist

we have a general thread here about probability theory in Coq: https://coq.discourse.group/t/finite-discrete-probabilities-in-coq/166

Guillaume and I know each other already, and I advised him to admit anything he needs in complex analysis and measure theory. I also pointed him to your PR @Reynald Affeldt . Meanwhile this is another motivation to get through complex analysis. I also thought that anything serious in probability theory could interest @Pierre-Yves Strub , but I might be wrong.

Thank you for these references! It looks like these repositories already contain some useful things. May I ask your opinion about the following (quite recent) work:

https://www.researchgate.net/publication/330431409_Formalizing_Probability_Concepts_in_a_Type_Theory

I wondered if this approach was at all compatible with mathcomp (which is not mentioned). But more fundamentally, I would like to know a correct syntax to work with (general, so possibly continuous) random variables. For instance, has the Central Limit Theorem ever been formalized in Coq?

Central Limit Theorem has not been formalized in Coq to my knowledge, just in Isabelle. From a cursory look at the link, this looks like a workshop-or-below l evel paper (a telltale sign is that there are no references at all to the papers on probability in Coq that existed in 2018, most blatantly ALEA which is from 2007)

Haven;t seen that work before. Did anyone contact the author?

Last updated: Feb 05 2023 at 08:28 UTC