>>667 追加
>while many LANA members hold the view that “the original paper does not contain at least a formalizable proof,” the members were unable to reach complete consensus on this point.
>さらに、「abc予想」の証明が存在するか否かという点については、多くのLANAメンバーが「元の論文には、少なくとも形式化可能な証明は含まれていない」という見解を抱いているものの、メンバー間でこの点に関する完全な合意に至ることはできなかった。

さて
・要するに、数学が議会のように 多数決で決まるならば、否決なのだろうが
・” the members were unable to reach complete consensus on this point.”は、加藤文元さんがガンバッたかもです
・ともかく、Leanに落とせない ←→ many LANA members hold the view that “the original paper does not contain at least a formalizable proof”
　なのでしょうね
・だが、LANA membersは 「何か足りないが、何かを足せば Lean化可能」と
　例えば、P49 10.5. Provisional assessment.
"On the other hand, our analysis does not give rise to this particular diagram; rather,
the elaboration of the η-algorithm shows that the proof of the final numerical inequality
hinges on the compatibility (9-1) which is not manifestly false. However, we, the LANA
project, do not have a proof of (9-1) at this time."
(google訳)
”一方、我々の解析からは当該の図式は導かれません。むしろ、η-アルゴリズムを詳細に検討すると、最終的な数値的不等式の証明は、明らかに誤りとは言えない整合性条件 (9-1) が成立するかどうかにかかっていることがわかります。しかしながら、LANAプロジェクトである我々は、現時点では (9-1) の証明を持っていません。”
より
これから、 (9-1) の証明を追加できれば OKとも読める
（これは一例）

まあ、ともかく 望月さんの側（単に一個人でなくグループで）が、何が問題なのかを きちんと把握して
対処するべし
それに尽きるのでは？