>>534 補足
へんなやつらが湧いているな

追加しておくと
１）IUTを なんらかのコンピューター証明に乗せられないか？
　という案だけは、望月氏のIUT論文投稿後 随分初期からあった（10年以上前）
　が、当時のコンピューター環境では、コンピューター証明に乗せるには
　マンパワーとマシンパワーが足りなかっただろう（だれも出来なかった）
２）2026年の今は、Lean形式化と AIのアシストと マシンパワーで
　ようやく IUTの検証が可能なレベルになってきたのでしょうね
３）さて、先の中間報告 7月17日 >>327 ご参照方
　中間報告の結論は、現時点のLean形式化未達なれど 達成できる可能性はあるという

よって
１）みんなで手分けして 早く結論を出した法が良いだろう
　そうしないと、望月研の院生とか「おれたちどうなるの？」って話とかね
２）軌道修正の余地はあるのでは？
　現時点のギャップを埋めるライブラリー補充とか
　ギャップを迂回する別ルートを探すとか
３）いまどきなら AIエージェント使いをリクルートして
　AIエージェントを走らずとかもありだろう

収束を加速する手段は、いろいろ考えられるから
議論をオープンにすれば良いと思うよ