Skip to content

Add Erdős Problem 603 (chromatic Property B for intersection ≠ 2)#3776

Open
henrykmichalewski wants to merge 1 commit intogoogle-deepmind:mainfrom
henrykmichalewski:add-problem-603
Open

Add Erdős Problem 603 (chromatic Property B for intersection ≠ 2)#3776
henrykmichalewski wants to merge 1 commit intogoogle-deepmind:mainfrom
henrykmichalewski:add-problem-603

Conversation

@henrykmichalewski
Copy link
Copy Markdown
Member

@henrykmichalewski henrykmichalewski commented Apr 16, 2026

fixes #822

Problem

Erdős Problem 603: https://www.erdosproblems.com/603 (sister problem of 602)

Does every family of sets, any two of which intersect in at most 2 points, have chromatic Property B?

Contents

  • HasChromaticPropertyB definition generalizing Problem 602
  • Main open theorem erdos_603
  • Komjáth's ≠1 intersection result as context
  • 4 proved variants (finite family, singleton family, pairwise disjoint, large sets)
  • Disproof of a misformalization (showing the naive encoding is too weak)
  • Sanity checks ensuring definitions are non-trivial

Assisted by Claude (Anthropic).

…ion ≠ 2

Adds formalization of Erdős Problem 603 (sister problem of 602).
Reference: https://www.erdosproblems.com/603

Asks whether every family of sets, any two of which intersect in at most
2 points, has chromatic Property B. Includes HasChromaticPropertyB
definition generalizing 602, Komjáth's ≠1 result as context, 4 proved
variants, disproof of a misformalization, and sanity checks. Assisted by
Claude (Anthropic).
@github-actions github-actions bot added the erdos-problems Erdős Problems label Apr 16, 2026
@henrykmichalewski
Copy link
Copy Markdown
Member Author

Closes #822

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

erdos-problems Erdős Problems

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Erdős Problem 603

1 participant