ミザールに聞いてみるか？
http://fm.ee.ibaraki.ac.jp/

例
JORDAN曲線定理（1887、仏カミーユ・ジョルダン）
「閉じた曲線が平面を、内と外に分ける」直感的には明らかな定理
Oswald Veblenが1905年に一応の証明をしたと言われていますが
前提となる 知識の至るところに直感が使われ、完全証明とは言いがたいものでした。
Mizarによるコンピュータを使った証明は、このような人間の直感を排除し
正確な証明を導き出すことができるのです。

1991年、日本の信濃大学、中村八束教授らや
ポーランドのワルシャワ大学の研究チームらが
14年かけて証明を終えた。