Problems/Erdos-Renyi Random Graph Model

Erdos-Renyi Random Graph Model

ProbabilitySOLVED
Year
1959
Difficulty
*****
Solved by
Paul Erdos & Alfred Renyi (1959)

Statement

In G(n,p), a sharp phase transition occurs at p = 1/n: a giant component emerges.

G(n,p):  p=cn⇒{small componentsc<1giant componentc>1G(n,p):\; p=\frac{c}{n} \Rightarrow \begin{cases} \text{small components} & c<1 \\ \text{giant component} & c>1 \end{cases}

About this Problem

Foundation of random graph theory and modern network science. Predicts when connected components suddenly emerge.

About the Lean 4 Prover

Lean 4 is a theorem prover and programming language. When a proof compiles in Lean, it is mathematically certain to be correct — the type checker verifies every logical step. This is the gold standard for formal verification.

Our platform uses fal.ai serverless compute to run Lean verification, and Gemini to generate proof strategies that are then formally checked. ShinkaEvolve provides the evolutionary backbone for automated mathematical discovery.

Mathematical Art

Generate a unique AI illustration of this problem using fal.ai FLUX.

Connected Constellations