ラムゼーの有名なやつ とは
「6人いれば、互いに知り合いである3人組か、互いに知り合いでない3人組が存在する」
というものです。
グラフ理論の言葉で言うと、
「完全6点グラフの各辺を赤か青に彩色したとき、どんな塗り分けに対しても、
赤一色の三角形か、青一色の三角形が存在する」
となります。
証明は以下です。 （Wikipediaより）
6つの点があり、その中のどの2つの点も赤い線か青い線で結ばれているとする。
赤一色の三角形か青一色の三角形が存在することを示せばよい。
6つの点のうち、どれでも良いので1つの点に着目し、その点をAとする。
Aからは5本の線が出ているので、そのうちの3本以上は同じ色の線である筈である。
.
Aから赤い線が3本以上出ている場合を考える。
Aと赤い線でつながっている点は3つ以上あるが、そのうちの3点をB,C,Dとする。
BとCが赤い線で結ばれている場合、三角形ABCはどの辺も赤い赤一色の三角形である。
CとD、DとBが赤い線で結ばれている場合も同様に赤一色の三角形が存在する。
よって、B,C,Dの中のいずれか2点が赤い線で結ばれている場合は赤一色の三角形が存在する。
そうでない場合、即ち、B,C,Dのうちどの2点も青い線で結ばれている場合、
三角形BCDはどの辺も青い青一色の三角形である。
よってこの場合も一色の三角形が存在する。
.
Aから青い線が3本以上出ている場合も同様である。
図を描くと分かりやすいです。
.
.
これをEgisonで証明します。
まず、Aから赤い線が3本以上出ている場合を考えます。
これらの線に1, 2, 3の名前を付けます。
これらの線に繋がっている三角形を4, 5, 6とし、
4, 5, 6のどんな塗り分けに対しても、
赤一色の三角形か、青一色の三角形が存在する事を言います。
.
.
公式ドキュメントにも載っている例です。 4,5,6を二つの集合に分けたと解釈できます。 第一集合を、辺を赤に塗ったもの、第二集合を、辺を青に塗ったものとします。 > (match-all {4 5 6} (multiset integer) [<join $xs $ys> {xs ys}]) {{{} {4 5 6}} {{4} {5 6}} {{5} {4 6}} {{6} {4 5}} {{4 5} {6}} {{4 6} {5}} {{5 6} {4}} {{4 5 6} {}}} >
この出力の各第一集合（赤）に{1 2 3}と、インデックス100～107番を加えます。
それに対して三角形(456, 412, 523, 631)が存在するかパターンマッチします。
全てのインデックス100～107番が出力されれば、証明完了です。
.
.
.
.
