Erdős Problem 1177: Chromatic Numbers of 3-Uniform Hypergraphs

### What is the conjecture

Let $G$ be a finite 3-uniform hypergraph, and let $F_G(\kappa)$ denote the collection of 3-uniform hypergraphs with chromatic number $\kappa$ not containing $G$ as a subhypergraph.

**Conjecture (1) - Cardinality bound:** If $F_G(\aleph_1)$ is non-empty, then there exists $X \in F_G(\aleph_1)$ of cardinality at most $2^{2^{\aleph_0}}$.

**Conjecture (2) - Intersection property:** If both $F_G(\aleph_1)$ and $F_H(\aleph_1)$ are non-empty, then $F_G(\aleph_1) \cap F_H(\aleph_1)$ is non-empty.

**Conjecture (3) - Cardinal transfer property:** For uncountable cardinals $\kappa$ and $\lambda$, if $F_G(\kappa)$ is non-empty, then $F_G(\lambda)$ is non-empty.

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

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

### Prerequisites needed

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

Building blocks (1-3; from search results):
- `Fintype` and combinatorial structures for hypergraphs in Mathlib
- `Cardinal` definitions for uncountable cardinals ($\aleph_0$, $\aleph_1$, cardinal exponentiation)
- Basic set theory definitions

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of $k$-uniform hypergraph and subhypergraph containment for infinite structures
- Definition of chromatic number for 3-uniform hypergraphs and the class $F_G(\kappa)$

Rating justification (1-2 sentences): The foundational concepts (cardinals, basic combinatorics) exist in Mathlib, but formalizing the statement requires defining 3-uniform hypergraphs and their chromatic numbers in the context of infinite cardinality constraints, which requires moderate additional infrastructure. The three conjectures themselves are clearly stateable once these definitions are in place.

### [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)