Add Erdős Problem 596 (characterize graphs with finite-vs-countable Ramsey gap)#3783
Add Erdős Problem 596 (characterize graphs with finite-vs-countable Ramsey gap)#3783henrykmichalewski wants to merge 5 commits intogoogle-deepmind:mainfrom
Conversation
… Ramsey gap Formalises Problem 596 asking which pairs (G, H) have finite Ramsey number for G but arbitrarily large finite Ramsey numbers only when the size grows, jumping to ℵ₀ in the countable case. Introduces predicates HasFiniteRamseyProperty, HasCountableRamseyEscape, and IsErdosHajnalExceptional, and records (C₄, C₆) as an example via the Nešetřil-Rödl and Erdős-Hajnal results, with the link to Problem 595 for (K₄, K₃). Reference: https://www.erdosproblems.com/596 Assisted by Claude (Anthropic).
|
Closes #815 |
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.
| @@ -0,0 +1,229 @@ | |||
| /- | |||
| Copyright 2025 The Formal Conjectures Authors. | |||
There was a problem hiding this comment.
nit: Could you update the copyright year to 2026 for this new file?
| **Status:** OPEN. | ||
| -/ | ||
| @[category research open, AMS 5] | ||
| theorem erdos_596 : answer(sorry) ↔ |
There was a problem hiding this comment.
Does Problem 596 ask for which pairs (G₁, G₂) have the two properties? As written, this only asks for existence of at least one exceptional pair, which the later (C₄, C₆) variant already supplies. Could you make the main statement record the unknown characterization, perhaps by putting the class of exceptional pairs itself behind answer(sorry)?
Paul-Lez
added
the
awaiting-author
…ok] + copyright 2026 Per Paul-Lez review on PR google-deepmind#3783. Mechanical nits applied on top of an upstream/main merge to pick up the new attribute infrastructure (google-deepmind#3900).
|
@Paul-Lez — applied the mechanical nits in |
…review) The headline previously asked only for the existence of one exceptional (G₁, G₂) pair, which is already supplied by the (C₄, C₆) variant. Per Paul-Lez's review, the source asks for a characterization of all exceptional pairs. The headline now asserts equivalence with a conjectural predicate behind answer(sorry), and the existence statement is demoted to a named variant.
|
Thanks for the review @PaulLez. Pushed 066b374 on |
mo271
removed
the
awaiting-author
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Nice formalization with good coverage of the known results! A few issues:
- Edge-colouring definitions miss disjointness (potential misformalization)
IsNEdgeColouring and IsCountableEdgeColouring define a colouring as H = ⨆ i, c i, which only requires the colour classes to cover H — the same edge can appear in multiple colour classes. A proper edge-colouring should partition the edges. This matters because:
For the Ramsey direction: quantifying over all covers (not just partitions) makes HasFiniteRamseyProperty stronger than intended.
For the escape direction: finding a cover (not a partition) is easier, making HasCountableRamseyEscape weaker than intended.
The combined effect means IsErdosHajnalExceptional may not be equivalent to the mathematical definition. Consider requiring at minimum (∀ i, c i ≤ H) ∧ H ≤ ⨆ i, c i, or ideally adding pairwise disjointness of the c i.
- ContainsCopy / IsFree duplicate Mathlib API
Mathlib already provides SimpleGraph.IsContained (notation G ⊑ H) and SimpleGraph.Free in Mathlib.Combinatorics.SimpleGraph.Copy with full API (transitivity, monotonicity, congruence, etc.). The custom ContainsCopy and IsFree are definitionally identical and should be replaced.
- Problem statement repeated 3×
The problem appears in the verbatim quote (line 23), the "Overview" section (lines 41–46), and the erdos_596 docstring (lines 126–148). Per project conventions, it should appear only once; variant-specific context should go in the respective variant docstrings.
- Universe mismatch
The main erdos_596 quantifies over Type but original_conjecture_is_false quantifies over Type*. These should be consistent.
3 participants
Formalises Erdős Problem 596: characterize the pairs of graphs$(G, H)$ exhibiting a finite-to-countable Ramsey gap.
Contents
HasFiniteRamseyPropertyHasCountableRamseyEscapeIsErdosHajnalExceptionalAssisted by Claude (Anthropic).