ずっと昔に、四色問題はたしかだれかが証明をしたというのがあって。証明されたものとして50年間経って、
実は証明に穴があるということが発見されて、それからがかなり苦難の道であった。そうして大勢のアマチュア
も含めて証明する努力が続けられたがついに、ということになっている。あれもLEANでも証明を再確認された
のだろうか？不可避集合の分類と列挙、それらの塗り分け可能性の証明というような。もちろんまるで違う
証明法がAIによって新しく発見されたらそれはそれで面白いと思う。