Erdős problem 78: Constructive proof for asymptotics of diagonal Ramsey number

### What is the conjecture

https://www.erdosproblems.com/78

Give a constructive proof that $R(k)>C^k$ for some constant $C>1$.

### Prerequisites needed
- not entirely sure how "constructive proof" is to be formalized here
- Needs the definition of the Ramsey number $R(k)$, which is currently not in Mathlib, but will also be useful in other Erdős problems, like #306

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else