遠アーベル幾何学の形式化という大きな企画がまずあって
遠アーベル幾何学を核として構成されているIUT理論の形式化もふくまれている
加藤さんの発言からするとIUT理論の妥当性はLEAN形式化側からは断言できないとされるから
abc予想の解決以上にIUT理論は正しいの？応用豊富なの？というところが結構焦点だよね
遠アーベル幾何学の形式化はうまくいってもIUTの形式化は困難となると問題だろうな
加藤さんは望月さんの友人としてきちんと数学界で共通認識を得ようとつまり白黒つけようと
LEAN形式化という舞台をもったのだろうからこれからどうなるのか興味深い
でも何年もかかりそうですな