>>32
この日経の記事で

>数学の超難問の「ABC予想」に関連する「宇宙際タイヒミューラー（IUT）理論」や「遠アーベル幾何学」の主要な定理をプログラミング言語の「Lean」で記述できるようにする。超難問の証明過程をLeanで正確に記述できれば、証明の真偽を確かめられる。

とあるのだけどこれは誤解
・上手く形式化できて証明出来る
・上手く形式化できない
・形式化が下手なのか
・証明に問題があるから形式化が不可能なのか
の後者は簡単に決着付かない
証明できる人間がまだ出てない問題は偽であると言えないのと同じ
その過程で何処に問題があるのかははっきりしてくる
しかしそれがSS論文の結論に近いというのが現在の状況