コンピュータ計算による網羅的な探求の例としては，以下の２つの有名な極値問題が解決されたことがあげられる．

(1)１９８８年，ヘールズはケプラーの球の詰め込み問題（１６１１年）が正しいことを示した．

(2)１９７６年，ハーケンとアッペルは４色問題（１８５２年）が正しいことを示した．

　その後，ロバートソン，サンダース，シーモア，トーマスによって証明が簡略化されたが，依然，コンピュータに依存した証明である．

　　［参］グラフマイナー，「離散数学のすすめ」第１２章，現代数学社

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝

【１】クラトウスキーの定理

　「与えられたグラフＧが平面グラフである必要十分条件は，ＧがＫ3,3とＫ5をマイナーとして含まないことである．」

　Ｋ3,3とＫ5は平面上に枝を交差させることなく描くことができないし，平面上に描くことさえできない．この定理を使うと４色定理は

　「Ｋ3,3とＫ5をマイナーとして含まないグラフは，頂点を４色で彩色することが可能である．」と言い換えることができる．

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝

【２】ワグナーの分解定理

　「Ｋ5をマイナーとして含まないグラフは，平面グラフと８点からなる特殊なグラフから生成可能である．」

　この定理より「Ｋ5をマイナーとして含まないグラフは，頂点を４色で彩色することが可能である．」が４色定理と同値であることがわかる．

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝

【３】ハドヴィガー予想（１９４３年）

　「Ｋkをマイナーとして含まないグラフは，頂点を（ｋ−ｌ）色で彩色することが可能である．」

　ｋ＝５の場合が４色定理に相当しますから，ｋ≧６の場合は４色定理より強いことを主張しているというわけである．１９９３年に，ロバートソン，シーモア，トーマスによってｋ＝６の場合が証明された．ｋ≧７の場合は現在解明されていない重要な問題の中で，最も難しい予想のひとつと考えられている．

　さらに，ロバートソンとシーモアはハドヴィガー予想が多項式時間で解決可能であることを証明した．このように彼らの取り組みは，離散数学の中でもとくにグラフ理論，アルゴリズム分野において数多くの深遠な結果と大きな前進をもたらしたのである．

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝