From a purely technical point of view, the essence of LeanForm —atleast in the case of IUT — lies in undertaking a fundamental reorganization of the theory into suitable purely formal/combinatorial blackboxes
純粋に技術的視点から、Lean形式の核心は−少なくともIUTの場合−理論の、適切で純粋に形式的/組合せ的なブラックボックス群（数学の群ではなく”むれ”の意）への抜本的再編制を保証することの中にある

要するに「理論をブラックボックス群へ再編制することがLean形式化の核心だ」と言っている。
それは別に否定しないが、ブラックボックスはあくまでブラックボックスだから、最終ゴールである完全形式化に向けての（かなり手前の）中間ゴールだろと思う。
しかもその中間ゴールへの途上で早くも「超えられない壁」にブチ当たっている。
つまり「最終ゴールは遥か彼方にあって今の段階では目途の立て様が無い」という進捗ってことなんだろう。知らんけど。