つうか、実際の研究で形式化して論文書いているバカがいたらお目に
かかりたいと思うんだが。文keiの頭の中にしかいない数学者を批判さ
れても数学屋は困らないよ。