>>180
>https://news.yahoo.co.jp/articles/55ab428a6b745668d697cd8553272d9edcf22155
>news.yahoo
>ABC予想証明の正否、コンピューターで決着か　望月氏が打開策示す
>1/2(金) 朝日新聞 （石倉徹也）

石倉記事より 引用下記
『こうした研究は数十年前に始まり、coqやHOLなどの「証明チェッカー」が登場してきた。検証の正しさは、数理論理学によって裏付けられており、過去には「ケプラー予想」や「四色定理」について、数学者の証明が検証された。』
『道のりは険しい。証明をコードに直す形式化は、複雑な式をコードに翻訳する骨の折れる作業で、ケプラー予想の場合は数十人で約10年かかった。今回のIUT理論は、700ページ以上あり、「どこがわからないのかさえわからない」と言われた難しさだ』

・「ケプラー予想」や「四色定理」は、下記の 計算機援用証明であって
　コンピュータを使った 形式的検証ではないぞ
・だから、”ケプラー予想の場合は数十人で約10年かかった”は 全く違う話だよ
・かつ いまはAIで文章を読ませる前処理を使える可能性があるので
　数十人で約10年は 非該当
・「どこがわからないのかさえわからない」もおかしい
　著者の望月氏自身が全面協力することなのだから

　(参考)>>135より 再録
https://ja.wikipedia.org/wiki/%E8%A8%88%E7%AE%97%E6%A9%9F%E6%8F%B4%E7%94%A8%E8%A8%BC%E6%98%8E
計算機援用証明
Wikipedia
計算機援用証明とは、コンピュータによって少なくとも一部が生成された数学的証明である。 今日における計算機援用証明のほとんどは数学的定理に対するしらみつぶし法（ ...
含まれない: 検証 ‎| 必須にする: 検証

https://ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E7%9A%84%E6%A4%9C%E8%A8%BC
形式的検証
Wikipedia
... 数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである。 完全な形式的検証 ...

https://ja.wikipedia.org/wiki/%E8%A8%BC%E6%98%8E%E8%AB%96
証明論
Wikipedia
形式的証明と非形式的証明​ 現代では、形式的証明は一般に計算機支援証明を補助としてコンピュータを使って構築される。 また、その証明がコンピュータで自動的に検証され ...