まあLean形式化はIUT論争を長引かせることが目的の確信犯的アクションなんじゃね？とも思えてしまう