望月氏は自分の数学が形式化できないものであることは理解してるんじゃないかな
（つまり標準的な数学者にとって氏の数学はアイディアの表現にすぎない）
ブログ等で以前から、自分の数学は19世紀の数学の継承であるとか、
人間の手に負える長さで形式化できるものは有限だけど数学は無限だとか、
形式化による機械検証を行ってもどうせ信用されないとか、
そういった類のことを言ってきてるから