26/07/26 23:11:09.43 jgtmOrU+.net
>>534 補足
へんなやつらが湧いているな
追加しておくと
１）IUTを なんらかのコンピューター証明に乗せられないか？
という案だけは、望月氏のIUT論文投稿後 随分初期からあった（10年以上前）
が、当時のコンピューター環境では、コンピューター証明に乗せるには
マンパワーとマシンパワーが足りなかっただろう（だれも出来なかった）
２）2026年の今は、Lean形式化と AIのアシストと マシンパワーで
ようやく IUTの検証が可能なレベルになってきたのでしょうね
３）さて、先の中間報告 7月17日 >>327 ご参照方
中間報告の結論は、現時点のLean形式化未達なれど 達成できる可能性はあるという
よって
１）みんなで手分けして 早く結論を出した法が良いだろう
そうしないと、望月研の院生とか「おれたちどうなるの？」って話とかね
２）軌道修正の余地はあるのでは？
現時点のギャップを埋めるライブラリー補充とか
ギャップを迂回する別ルートを探すとか
３）いまどきなら AIエージェント使いをリクルートして
AIエージェントを走らずとかもありだろう
収束を加速する手段は、いろいろ考えられるから
議論をオープンにすれば良いと思うよ