>>761
>どんだけゴミのために無駄なことすんだよゴミ

いやいや
今回のLANAチームの中間報告を見ると
１）ショルツェ氏のLeanでの論文検証をしたチーム(下記)が、IUT検証でダメだし
　（人間さまが10年以上グジグジ言ってきた問題をほぼ一刀両断した）
２）加えて 最近のAIによる数学の進化もある

なので、早く京大とRIMS（含次世代幾何学国際センター）で
数学コンピューター部隊専門チームを結成するべし
これは、一人IUTだけの問題ではない
京大とRIMS数学全体の問題でもある
そして、2027年度の大学及びRIMSの体制と予算の問題でもあるでしょう

(参考)
https://taro-nishino.blogspot.com/2023/01/blog-post096.html
taro-nishinoの日記
証明支援系が一流数学へと飛躍する
1月 02, 2023
(抜粋)
今日紹介する記事はQuantaのProof Assistant Makes Jump to Big-League Mathです。
https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/
何故、この記事を選んだかと言うと、皆さん御存知のペータ・ショルツェ博士が証明に対して実に真摯なことが分かるからです。そして、多忙にも拘わらず、協力すべき時は十分に協力をしてくれますので、さすが世界のリーダだと思います。日本の誰かさんとはえらい違いです。因みに前置きの海外知人はショルツェ博士のことを何年も前(勿論Fields賞受賞よりずっと前です)からI'm sure he'll make one of the greatest mathematicians in the maths annals. と言って非常に尊敬してました。ともかくも、その私訳を以下に載せておきます。