Erdős Problem 1174: Graph Coloring and Ramsey Properties

### What is the conjecture

Let $G$ be a graph. The conjecture asks two related questions:

**Question 1:** Does there exist a graph $G$ with no $K_4$ (complete graph on 4 vertices) such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_3$?

**Question 2:** More generally, does there exist a graph $G$ with no $K_{\aleph_1}$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_{\aleph_0}$?

These questions investigate the interaction between the chromatic properties of a graph (in the sense of avoiding certain complete subgraphs) and Ramsey-type properties under infinite colorings. The problem asks whether a graph can be "sparse" in one sense (avoiding large cliques) yet "dense" in another (forcing monochromatic cliques under any countable coloring).

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1174

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Graph types and complete subgraphs ($K_n$) are standard in Mathlib
- Edge coloring and finite colorings are available via `Fintype` and function types
- Infinite cardinals ($\aleph_0$, $\aleph_1$) are defined in Mathlib's set theory library

Missing pieces (exactly 2; unclear/absent from search results):
- Extension to countably infinite colorings (typically requires moving from `Fintype` to `Countable` or `Cardinal`-based definitions)
- Formalization of infinite Ramsey properties for arbitrary graphs with cardinal-indexed structure; existing Ramsey results in Mathlib are mostly finite or very specialized

Rating justification: The basic definitions (graphs, complete subgraphs, finite colorings) exist, but the infinite-cardinal version requires extending standard graph coloring formalism to countable and uncountable index sets, and the interaction between avoiding cliques and forcing monochromatic subgraphs under infinite colorings is non-standard.

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

* ams-05
* ams-03

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)