ブンゲンさんって日本語と英語で言ってることが微妙に違うよね
↓の英語では論文中に形式化可能な証明の記述がないことを
明言してるけど、日本語では「現状では不可能です」って
誰の責任か分からない曖昧な物言いになってる

それはそうとして、☆が詳細まで理解してるって設定は
どうなったんだよ

https://x.com/FumiharuKato/status/2078016732661424271
＞Fumiharu Kato 加藤文元（Bungen）
＞@FumiharuKato 4:19 PM · Jul 17, 2026
＞本日の記者会見のまとめです：
＞我々の過去2年間にわたる取り組みの結論ですが、IUT論文において
＞定理3.11から系3.12に至る論証のコンピューター形式化は現状では
＞不可能です。しかし、この点に関する望月氏の追加説明が今も
＞続いているため、現時点では最終的な判断を留保しています。
https://x.com/FumiharuKato/status/2078017230537892207
＞Fumiharu Kato 加藤文元（Bungen）
＞@FumiharuKato 4:21 PM · Jul 17, 2026
＞In today's press conference, we explained our efforts over
＞the last two years which resulted in the following conclusion:
＞The way the argument from Theorem 3.11 to Corollary 3.12 is
＞written in the IUT papers is unformalizable. But since
＞Mochizuki's explanation of this point has recently started
＞evolving, we reserve final judgement at this time.
【Google翻訳】本日の記者会見では、過去2年間の取り組みについて
説明し、以下の結論に至りました。IUT論文における定理3.11から
系3.12への議論の記述方法は形式化不可能である。しかしながら、
望月氏によるこの点に関する説明が最近になって進展し始めたため、
現時点では最終的な判断を保留する。