random_graphs Formalizing the Erdős–Rényi random graph model in Lean4. Useful resources: Yael's formalization of random graphs. Bernoulli PMF in mathlib. Moogle for searching mathlib. GitHub Copilot for generating code. Free for students.