google-deepmind / google-deepmind/formal-conjectures
Erdős Problem 557
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 327
Description
### What is the conjecture
https://www.erdosproblems.com/557
Let $R(G;k)$ denote the minimal $m$ such that if the edges of $K_m$ are $k$-coloured then there is a monochromatic copy of $G$. Is it true that
$$R(T;k)=kn+O(1)$$
for any tree $T$ on $n$ vertices?
Status: open
### 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
Research direction
No files, tests, or entry points are mentioned. Start by reading the linked Erdős Problem 557 statement and the repository's contribution guidance; done means adding a formalized statement of the conjecture to the collection.
Written by the indexing model from the issue text.
Assessment
- Domain
- tooling
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100