MSが数学者として有能であることはもちろん否定しないが
だからといってIUTによるABC予想の証明が正しい
ということにはならない

加藤文元がなぜLANAプロジェクトを推進するのかその理由は明確でない
形式化によってIUTの正当性が示されると本気で信じてるのかもしれない
もちろんそれは笑われるようなことではない

ただ、当人が「論文を読めば分かる」としか言わず
肝心な点については一切説明もしない態度をとり続けるのに
その証明の形式化がうまくいくと考えるのは
やはりお目出たいのではないだろうか