>>517
>あと4色問題は理論ですらない
>(コンピューターを使うと)しらみつぶしで証明できてしまったってだけ

分かってないな
「4色問題」は、”一松信『四色問題 どう解かれ何をもたらしたのか』講談社〈ブルーバックス B-1969〉、2016”にも、書いてあったと思うが
おそらく、「コンピュータを使用しない証明は、得られない！」 最初の例になるのではないかといわれている
「4色問題」は、これはこれで意義があると思う。定理証明系Coqなどにも繋がっている
そういう意味で、「コンピュータしらみつぶし」証明の歴史を開いた意義があると思う
（なお、よく言われるのが、自然数ｎに関連する定理で、一般論が通用ぜず、n=３，４，５辺りが例外事象が多く、証明が難しくなることがあると）

（参考）
https://ja.wikipedia.org/wiki/%E5%9B%9B%E8%89%B2%E5%AE%9A%E7%90%86
(抜粋)
厳密ではないが日常的な直感で説明すると「平面上のいかなる地図も、隣接する領域が異なる色になるように塗り分けるには4色あれば十分だ」という定理である。

歴史
1976年にケネス・アッペル とヴォルフガング・ハーケンは、コンピュータを利用して約2000個の（後に1400個あまりに整理された）可約な配置からなる不可避集合を見出し、四色定理を「証明」するに至った
人手による実行が（事実上）不可能なほどの複雑なプログラムの実行によるものであることから、ハードウェアやソフトウェア（コンピュータやそのプログラム）のバグの可能性などの懸念から、その確実さについて疑問視する向きもあった。
2004年にはジョルジュ・ゴンティエ (Georges Gonthier) が定理証明系Coqを用いて、よりシンプルな証明を行う

証明
複雑に思える問題に対して簡潔にまとまった比較的短い証明（解答）を、エレガントな証明（解答）と言うことがある。
四色定理のある種「力業な証明」は、これと対極にあるものとして揶揄を込めて「エレファント（象）」な証明とも言われた。
5色による塗り分けが可能であることの証明が簡潔なものであるのと対照的である。

現在でもコンピュータを使用しない証明は得られていない
それどころか完全に自然言語を離れて、プログラムにバグがないことも含めた四色定理の証明全体をコンピュータに打ち込んで証明検査器Coqにチェックさせた仕事がある