望月新一に「LeanでIUTを形式化したいんですけど、ここのギャップってどうやって埋めるんですか？」って聞いたらどうなるの