Add Erdős Problem 595 (K₄-free graph not union of triangle-free, $250 prize) by henrykmichalewski · Pull Request #3775 · google-deepmind/formal-conjectures

henrykmichalewski · 2026-04-16T12:24:16Z

fixes #814

Problem

Erdős Problem 595: https://www.erdosproblems.com/595 ($250 prize)

Does there exist a K₄-free graph of chromatic number ℵ₁ which cannot be written as a countable union of triangle-free subgraphs?

…e-free ($250 prize) Adds formalization of Erdős Problem 595 (Erdős-Hajnal, $250 prize). Reference: https://www.erdosproblems.com/595 Asks whether there exists a K₄-free graph of chromatic number ℵ₁ which cannot be written as a countable union of triangle-free subgraphs. Includes IsCountableUnionOfTriangleFree definition, Folkman/Nešetřil-Rödl finite version, 4 proved lemmas, and edge-colouring reformulation. Assisted by Claude (Anthropic).

henrykmichalewski · 2026-04-17T08:23:39Z

Closes #814

mo271

Thanks! Looks good to me and mathemtically correct, just some small suggestions...

mo271

Thanks, LGTM!

mo271 · 2026-04-17T13:12:47Z

CLA bot is not happy -- should be fixed by rewriting history, removing authors that have not signed the CLA by amending the commit(s)...

…e_colouring - Update copyright year to 2026 - Remove duplicate docstring on IsCountableUnionOfTriangleFree def - Update reformulation_edge_colouring docstring to reference c : G.edgeSet → ℕ - Change attribute to @[category test, AMS 5] - Prove reformulation_edge_colouring using EdgeLabeling.iSup_labelGraph and Sym2.ind Assisted by Claude (Anthropic).

Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.

Paul-Lez

Note: some of the attribute infrastructure has changed, so you'll want to merge main and fix things. Apart from that I think this is ready to merge!

Paul-Lez · 2026-05-07T17:14:08Z

+**Proof**: If `G = ⨆ i, G_i` with each `G_i` triangle-free, then `H = ⨆ i, H ⊓ G_i`.
+Each `H ⊓ G_i` is triangle-free because it is a subgraph of `G_i`.
+-/
+@[category undergraduate, AMS 5]


nit: Looks like this file still uses @[category undergraduate] for a few auxiliary/supporting lemmas. This now no longer works on main - the new version of this is textbook.

… textbook] Per Paul-Lez review on PR google-deepmind#3775. The 'undergraduate' category was renamed to 'textbook' on upstream/main in google-deepmind#3900. This commit, on top of the just-merged upstream/main, applies the rename to the four supporting-lemma decorators in this file. Builds cleanly: lake build FormalConjectures.ErdosProblems.«595»

henrykmichalewski · 2026-05-08T00:50:22Z

@Paul-Lez — applied your two follow-ups in 0ba9785, on top of the maintainer-merged main. The four @[category undergraduate] decorators are now @[category textbook], and the file builds cleanly against the new attribute infrastructure. Should be ready to merge.

mo271

LGTM up to some docstring changes, see suggested changes (some of which are the same as made before in the initial review)

mo271 · 2026-05-03T13:12:38Z

+a positive answer.
+
+**Open question:** Whether the *infinite* version holds — i.e., whether a single graph can
+simultaneously be $K_4$-free and not expressible as a countable union of triangle-free graphs.


Suggested change

simultaneously be $K_4$-free and not expressible as a countable union of triangle-free graphs.

Let's not duplicate the docstrings in the module header

mo271 · 2026-05-03T13:13:41Z

+**Formalization:** We ask for the existence of an infinite type `V` (witnessed by `[Infinite V]`)
+and a `SimpleGraph V` that is $K_4$-free (`G.CliqueFree 4`) but not a countable union of
+triangle-free graphs.
+
+**Prize:** \$250 (see erdosproblems.com/595).
+
+**Status:** OPEN.
+
+**Known (Folkman [Fo70], Nešetřil–Rödl [NeRo75]):** For every finite `n ≥ 1`, there exists a
+graph (even a finite one) that is $K_4$-free but not a union of `n` triangle-free graphs. This
+is the variant `erdos_595.variants.folkman_finite`. However, whether `n` can be replaced by
+`ℵ₀` (countably infinite) is the content of this open problem.


Suggested change

**Formalization:** We ask for the existence of an infinite type `V` (witnessed by `[Infinite V]`)

and a `SimpleGraph V` that is $K_4$-free (`G.CliqueFree 4`) but not a countable union of

triangle-free graphs.

**Prize:** \$250 (see erdosproblems.com/595).

**Status:** OPEN.

**Known (Folkman [Fo70], Nešetřil–Rödl [NeRo75]):** For every finite `n ≥ 1`, there exists a

graph (even a finite one) that is $K_4$-free but not a union of `n` triangle-free graphs. This

is the variant `erdos_595.variants.folkman_finite`. However, whether `n` can be replaced by

`ℵ₀` (countably infinite) is the content of this open problem.

mo271 · 2026-05-10T07:59:13Z

+**Verbatim statement (Erdős #595, status O):**
+> Is there an infinite graph $G$ which contains no $K_4$ and is not the union of countably many triangle-free graphs?
+
+**Source:** https://www.erdosproblems.com/595
+
+**Notes:** OPEN - $250
+
+


Suggested change

**Verbatim statement (Erdős #595, status O):**

> Is there an infinite graph $G$ which contains no $K_4$ and is not the union of countably many triangle-free graphs?

**Source:** https://www.erdosproblems.com/595

**Notes:** OPEN - $250

mo271 · 2026-05-10T07:59:42Z

+*Reference:* [erdosproblems.com/595](https://www.erdosproblems.com/595)
+
+*References for known results:*


Suggested change

*Reference:* [erdosproblems.com/595](https://www.erdosproblems.com/595)

*References for known results:*

*References:*

- [erdosproblems.com/595](https://www.erdosproblems.com/595)

mo271 · 2026-05-10T08:01:16Z

+## Overview
+
+**Problem (Erdős–Hajnal, $250)**: Is there an infinite graph $G$ which contains no $K_4$
+and is not the union of countably many triangle-free graphs?
+
+The "union of countably many triangle-free graphs" condition means that the edge set of $G$
+can be covered by countably many subgraphs, each of which is triangle-free (i.e., $K_3$-free).
+
+**Known (finite case):** Folkman [Fo70] and Nešetřil–Rödl [NeRo75] proved independently that
+for every $n \geq 1$ there exists a graph $G$ (which may be taken finite) that contains no $K_4$
+and whose edges cannot be coloured with $n$ colours such that each colour class is triangle-free.
+This means the *finite* version of the problem (with $n$ colours instead of countably many) has
+a positive answer.
+
+**Open question:** Whether the *infinite* version holds — i.e., whether a single graph can
+simultaneously be $K_4$-free and not expressible as a countable union of triangle-free graphs.
+
+See also [596] for the more general problem of which pairs $(G_1, G_2)$ exhibit this phenomenon.
+


Suggested change

## Overview

**Problem (Erdős–Hajnal, $250)**: Is there an infinite graph $G$ which contains no $K_4$

and is not the union of countably many triangle-free graphs?

The "union of countably many triangle-free graphs" condition means that the edge set of $G$

can be covered by countably many subgraphs, each of which is triangle-free (i.e., $K_3$-free).

**Known (finite case):** Folkman [Fo70] and Nešetřil–Rödl [NeRo75] proved independently that

for every $n \geq 1$ there exists a graph $G$ (which may be taken finite) that contains no $K_4$

and whose edges cannot be coloured with $n$ colours such that each colour class is triangle-free.

This means the *finite* version of the problem (with $n$ colours instead of countably many) has

a positive answer.

**Open question:** Whether the *infinite* version holds — i.e., whether a single graph can

simultaneously be $K_4$-free and not expressible as a countable union of triangle-free graphs.

See also [596] for the more general problem of which pairs $(G_1, G_2)$ exhibit this phenomenon.

## Overview

Let's not repeat the docstrings here (if we have the docstring only once there will be less work to keep them in sync when we change something...)

mo271 · 2026-05-10T08:02:33Z

+**Erdős Problem 595 ($250)**: Is there an infinite graph $G$ which contains no $K_4$ and is
+not the union of countably many triangle-free graphs?
+
+A problem of Erdős and Hajnal [Er87].
+
+**Formalization:** We ask for the existence of an infinite type `V` (witnessed by `[Infinite V]`)
+and a `SimpleGraph V` that is $K_4$-free (`G.CliqueFree 4`) but not a countable union of
+triangle-free graphs.
+
+**Prize:** \$250 (see erdosproblems.com/595).
+
+**Status:** OPEN.
+
+**Known (Folkman [Fo70], Nešetřil–Rödl [NeRo75]):** For every finite `n ≥ 1`, there exists a
+graph (even a finite one) that is $K_4$-free but not a union of `n` triangle-free graphs. This
+is the variant `erdos_595.variants.folkman_finite`. However, whether `n` can be replaced by
+`ℵ₀` (countably infinite) is the content of this open problem.


Suggested change

**Erdős Problem 595 ($250)**: Is there an infinite graph $G$ which contains no $K_4$ and is

not the union of countably many triangle-free graphs?

A problem of Erdős and Hajnal [Er87].

**Formalization:** We ask for the existence of an infinite type `V` (witnessed by `[Infinite V]`)

and a `SimpleGraph V` that is $K_4$-free (`G.CliqueFree 4`) but not a countable union of

triangle-free graphs.

**Prize:** \$250 (see erdosproblems.com/595).

**Status:** OPEN.

**Known (Folkman [Fo70], Nešetřil–Rödl [NeRo75]):** For every finite `n ≥ 1`, there exists a

graph (even a finite one) that is $K_4$-free but not a union of `n` triangle-free graphs. This

is the variant `erdos_595.variants.folkman_finite`. However, whether `n` can be replaced by

`ℵ₀` (countably infinite) is the content of this open problem.

**Erdős Problem 595 ($250)**: Is there an infinite graph $G$ which contains no $K_4$ and is

not the union of countably many triangle-free graphs?

A problem of Erdős and Hajnal [Er87].

The price is mentioned also above, the formalisation note doesn't really ad anything

- Collapse the two reference blocks into a single *References:* block in the module docstring. - Drop the duplicated verbatim problem statement and the bloated Overview / Formalization-note sections from the module header. - Trim the Erdős Problem 595 theorem docstring to the short form mo271 suggested (problem statement + Erdős–Hajnal attribution), removing the Status/Prize/Formalization paragraphs already captured by the @[category research open] attribute and the verbatim quote in the docstring.

henrykmichalewski · 2026-05-10T17:35:13Z

Applied mo271's docstring-convention review pass in 70dd34c:

Lines 29, 32: collapsed the dual-reference scheme into a single *References:* block in the module docstring.
Line 59: removed the duplicated module-docstring ## ... overview block.
Line 97: replaced the bloated **Erdős Problem 595 ($250)** paragraph with the short Erdős–Hajnal form mo271 suggested; dropped the Status / Prize / Formalization-note paragraphs already captured by @[category research open] and the verbatim quote.

Build: lake build FormalConjectures.ErdosProblems.«595» is green. Should be ready to merge.

mo271

Thanks, lgtm now!

… prize) (google-deepmind#3775) fixes google-deepmind#814 ## Problem Erdős Problem 595: https://www.erdosproblems.com/595 ($250 prize) > Does there exist a K₄-free graph of chromatic number ℵ₁ which cannot be written as a countable union of triangle-free subgraphs? ## Contents - IsCountableUnionOfTriangleFree definition for SimpleGraph - Main open theorem `erdos_595` - Folkman/Nešetřil-Rödl finite version variant - Edge-colouring reformulation - 4 fully proved lemmas (empty graph is countable union, triangle-free implies countable union, finite clique-free graphs, monotonicity) Assisted by Claude (Anthropic). --------- Co-authored-by: Paul Lezeau <lezeau@google.com>

github-actions Bot added the erdos-problems Erdős Problems label Apr 16, 2026

mo271 approved these changes Apr 17, 2026

View reviewed changes

Comment thread FormalConjectures/ErdosProblems/595.lean Outdated

Comment thread FormalConjectures/ErdosProblems/595.lean Outdated

Comment thread FormalConjectures/ErdosProblems/595.lean Outdated

Comment thread FormalConjectures/ErdosProblems/595.lean Outdated

mo271 approved these changes Apr 17, 2026

View reviewed changes

henrykmichalewski force-pushed the add-problem-595 branch from 9887014 to bbb368b Compare April 19, 2026 09:55

henrykmichalewski and others added 2 commits April 22, 2026 14:42

Merge branch 'main' into add-problem-595

c2aaaa7

Paul-Lez enabled auto-merge (squash) May 7, 2026 15:00

Paul-Lez reviewed May 7, 2026

View reviewed changes

Paul-Lez added the awaiting-author The author should answer a question or perform changes. Reply when done. label May 7, 2026

henrykmichalewski mentioned this pull request May 8, 2026

Add Erdős Problem 593 (obligatory 3-uniform subhypergraphs, $500 prize) #3774

Open

auto-merge was automatically disabled May 8, 2026 00:50
Head branch was pushed to by a user without write access

mo271 approved these changes May 10, 2026

View reviewed changes

mo271 approved these changes May 11, 2026

View reviewed changes

mo271 merged commit 7134857 into google-deepmind:main May 11, 2026
6 checks passed

		Reference: [erdosproblems.com/595](https://www.erdosproblems.com/595)

		References for known results:

Conversation

henrykmichalewski commented Apr 16, 2026 • edited by mo271 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem

Contents

Uh oh!

henrykmichalewski commented Apr 17, 2026

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

mo271 commented Apr 17, 2026

Uh oh!

Paul-Lez left a comment

Choose a reason for hiding this comment

Uh oh!

Paul-Lez May 7, 2026

Choose a reason for hiding this comment

Uh oh!

henrykmichalewski commented May 8, 2026

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

mo271 May 3, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 May 3, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 May 10, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 May 10, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 May 10, 2026

Choose a reason for hiding this comment

Uh oh!

mo271 May 10, 2026

Choose a reason for hiding this comment

Uh oh!

henrykmichalewski commented May 10, 2026

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

henrykmichalewski commented Apr 16, 2026 •

edited by mo271

Loading