エレファント

Elephant

象のこと。

1976年にケネス・アッペルとヴォルフガング・ハーケンは、コンピュータによる実験を繰り返し、プログラムを何度も書き換えながら、可約なグラフから成る約2,000個のグラフからなる不可避集合を求めることで、四色定理を「証明」するに至った。当時の大型汎用コンピュータであるIBM System/370* を1,200時間以上使用したといわれている。

*これはスーパコンピュータではなく、特に最速でもない。

これは一応は認められたが、人手による実行が（事実上）不可能なほどの複雑なプログラムの実行によるものであることから、ハードウェアやソフトウェア（コンピュータやそのプログラム）のバグの可能性などの懸念から、その確実さについて疑問視する向きもあった。後年、第三者による複数の改良された証明が（コンピュータプログラムを用いているものの）何度も行われ、現在は四色問題は解決していると捉えられている。

そのあまりにも膨大な記述量に対してついた形容詞が elephant。

なお、現在は定理証明支援系 Coq や群論計算支援プログラム GAP の整備が進められ、コンピュータによる力技がなければ成し得ないような証明も度々見られる。