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