Add Erdős Problem 601 (infinite path or large independent set, $500 prize)

[henrykmichalewski]

Problem

Erdős Problem 601: https://www.erdosproblems.com/601 ($500 prize)

For which limit ordinals α is it true that if G is a graph with vertex set α, then G must have either an infinite path or an independent set on a set of vertices with order type α?

Contents

• Main open theorem erdos_601 ($500 prize note)
• New HasPathOrIndepSetOfType α definition
• Variants covering:
  • Erdős-Hajnal-Milner [EHM70]: TRUE for α < ω₁^(ω+2)
  • The specific $250 sub-case at α = ω₁^(ω+2)
  • Larson [La90] result under Martin's Axiom
  • Base case α = ω

Closes #820

Assisted by Claude (Anthropic).