Erdős problem 1105
The anti-Ramsey number is the maximum possible number of colours in which the edges of can be coloured without creating a rainbow copy of (i.e. one in which all edges have different colours).
Sources
FormalConjectures/ErdosProblems/
1105.lean
Retained formal statement
The anti-Ramsey number is the maximum possible number of colours in which the edges of can be coloured without creating a rainbow copy of (i.e. one in which all edges have different colours).
Let be the cycle on vertices. Is it true that ?
Montellano-Ballesteros and Neumann-Lara [MoNe05] gave an exact formula for , which implies in particular that
True ↔ ∀ (k : ℕ), 3 ≤ k → (fun n => ↑((SimpleGraph.cycleGraph k).antiRamseyNum n) - ((↑k - 2) / 2 + 1 / (↑k - 1)) * ↑n) =O[Filter.atTop] fun x => 1SolvedStatement only, no proof