まぁしかしiutの論文がちゃんとlean通るかどうか試したいというならやってみればいい。少なくとも通れば確実に数学界で大歓迎される偉大な仕事として歓迎されるやろ。なんやったらなんかの賞もらえるレベルの偉業になる。
問題は通らなかった場合。それでほんとに一億もらえるのかって話。まぁ無理やろ。数学の文章は適当に行間が空いてるのが普通でそこは自分で埋めなきゃ読めん。しかし普通の論文では空いていい行間に暗黙の了解があって通常の隙間は院生以上の能力が有れば埋められる。そして適宜行間を埋めればちゃんとleanに通せるコードを手に入れられる。
問題はそれができない場合。それが行間埋めに失敗してるのか、そもそも論文にエラーがあるのかで言い訳されてしまう。結局それやって通らなくても「それはお前の行間埋めが悪いだけ」と強弁されたら終わり。実際ショルツの指摘もそれで乗り切ってるしな。もちろんそんな言い訳数学の世界では通用しない。ある程度以上ぬ数学力持つものにならキチンと行間埋めができる範囲内でしか曖昧さは許されんしな。
今回の場合はそもそも本人が「通常の言語、推論即では読めない」と本人の書いてる文書にあるのでそもそもlean通らなくても当たり前と開き直られる可能性もあるしな。
まだアホ信者は「そのうち行間埋めてる資料が出る」とか言ってるけどいつまで寝言いうつもりなんですかねぇwwww