joshi は自分の論文を lean で書いてみせるといってるらしいから少なくともそれで一区切りつくわな。
失敗した場合に正直に「ダメでした」って報告があること前提だけど。
成功すればもちろん成功したコードを公開するだろうし、そのとき ABC の照明も一気に解決になる。こっちの可能性はまぁないだろうけど。