在今天的新闻发布会上，我们解释了过去两年的努力，得出了以下结论：IUT论文中从定理3.11到推论3.12的论证方式是无法形式化的。但由于望月对这一点的解释最近开始演变，我们在此时保留最终判断。在此次新闻发布会上，LANA展示的一个关键成就是我们为一般数学公众提供了对IUT理论中关键论证的可管理长度分析，该分析由外部人士撰写。该文档还包括与2018年Scholze-Stix报告的比较。YouTube 视频：youtube.com/live/KADN5NHmI… LANA报告：github.com/katobungen/LAN…