1:06:51〜で、ステージ１（3.11⇒3.12の形式化）に必要な時間は
"an ideal world"（LEAN熟練者がIUTを理解して形式化に協力する）では
半年〜１年以下だそうです
なにせ
>The logic of (supposedly difficult portions of) IUT
>is in fact very simple and elementary
ですから

IUTが理解不能であるという問題をLEANで解決するためには
LEAN熟練者がIUTを理解する必要があるということでしょうか？
エッシャーの階段です、モノドロミーの問題が生じています
この問題点をLEAN as a communication toolにより
解消できるというのが講演の主題でした