Formalize the Statement of the Shelah-Spencer theorem on 0-1 law of sparse random graphs

### What is the conjecture
For $\alpha \in [0,1]$, if $\alpha$ is irrational, the first order theory of Shelah-Spencer graphs $G(n, \alpha)$ admits a 0-1 law; if $\alpha$ is rational, that first order theory does not admit a 0-1 law. Here, $G(n, \alpha)$ is the random graph with edge probability $n^{-\alpha}$.

Reference: Zero-one Laws for Sparse Random Graphs, Journal of the American Mathematical Society, 1(1), 97-115. by S. Shelah and J. Spencer

### Prerequisites needed
Basic probability theory and combinatorics.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-03, ams-05

### Choose either option
- [Y] I plan on adding this conjecture to the repository