google-deepmind / google-deepmind/formal-conjectures
Erdős Problem 174
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 328
Description
### What is the conjecture
https://www.erdosproblems.com/174
A finite set $A\subset \mathbb{R}^n$ is called Ramsey if, for any $k\geq 1$, there exists some $d=d(A,k)$ such that in any $k$-colouring of $\mathbb{R}^d$ there exists a monochromatic copy of $A$. Characterise the Ramsey sets in $\mathbb{R}^n$.
Status: open
### Prerequisites needed
Not quite so clear what "Characerise" means here, perhaps it might be useful to formalize this using the `answer(sorry)` mechanism, possibly both as sufficient and necessary condition separately.
### 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
Contributor guide
Assessment
This issue has not been assessed yet.