Skip to content

Erdős problem 1105

The anti-Ramsey number AR(n,G)\mathrm{AR}(n,G) is the maximum possible number of colours in which the edges of KnK_n can be coloured without creating a rainbow copy of GG (i.e. one in which all edges have different colours).

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1105.lean

Retained formal statement1 of 2

The anti-Ramsey number AR(n,G)\mathrm{AR}(n,G) is the maximum possible number of colours in which the edges of KnK_n can be coloured without creating a rainbow copy of GG (i.e. one in which all edges have different colours).

Let CkC_k be the cycle on kk vertices. Is it true that AR(n,Ck)=(k−22+1k−1)n+O(1)\mathrm{AR}(n,C_k)=\left(\frac{k-2}{2}+\frac{1}{k-1}\right)n+O(1)?

Montellano-Ballesteros and Neumann-Lara [MoNe05] gave an exact formula for AR(n,Ck)\mathrm{AR}(n,C_k), which implies in particular that AR(n,Ck)=(k−22+1k−1)n+O(1).\mathrm{AR}(n,C_k)=\left(\frac{k-2}{2}+\frac{1}{k-1}\right)n+O(1).

FormalConjectures/ErdosProblems/1105.leanErdos1105.erdos_1105.parts.i5 linesExact file
True ↔  ∀ (k : ℕ),    3 ≤ k →      (fun n => ↑((SimpleGraph.cycleGraph k).antiRamseyNum n) - ((↑k - 2) / 2 + 1 / (↑k - 1)) * ↑n) =O[Filter.atTop]        fun x => 1
SolvedStatement only, no proof