Erdős 625: random graphs

Stream: Formal conjectures

[Moritz Firsching]

I'd like to add Erdős Problem 625. There we need definitions

1. Cochromatic number (also used in [a few other Erdős Problems])(http://erdosproblems.com/search/Cochromatic)
2. Random graph
   I gave it a try here:
   https://github.com/google-deepmind/formal-conjectures/pull/570

I thought sure random graphs with each edge included independently with probability $\frac 1 2$ must already be formalized somewhere, but a I couldn't find it.
Any hints?
Suggestion for improvements?

[Paul Lezeau]

Maybe @Yaël Dillies knows?

[Yaël Dillies]

I have some start in https://github.com/YaelDillies/LeanCamCombi/tree/master/LeanCamCombi/ExtrProbCombi, and a concurrent implementation of Bernoulli random variables in #28248. Basically right now there needs to be some thought on how to best represent Bernoulli random variables, so that it is painless to apply the setup to binomial random graphs

[Moritz Firsching]

Cool, thanks that is great. I will wait for at least #28248 then! The code in LeanCamCombi/ExtrProbCombi also looks reasonable.

[Moritz Firsching]

The Cochromatic definition is not in our ForMathlib, so the only missing part is the Erdős-Rényi model, which will also unblock a few other Erdős problems.