26/07/29 16:50:03.70 hkhoSbjD.net
>>626
>有限次元の線形空間を Leanで扱えるようにはなっても
>当然だが、無限次元は扱えない
>だから、例えば 無限次元ヒルベルト空間を扱うための
>Mathlib を整備すれば、その整備されたMathlibの範囲において
>無限次元ヒルベルト空間が扱えるってことだね
内容ゼロ
>これを、望月IUTにおいてみるに、まずIUT以外での
>確立された遠アーベルMathlib の整備が必要だね
関係無い。
系3.12（SS指摘部分）の形式化を目的に他部分を最大限ブラックボックス化したにもかかわらず大惨敗したのが今回の結果だから。
>そして
>その上で、今回のLANA中間報告のLean語でのコンピュータ証明の位置づけが問題だが
>上記ヒルベルトで言えば 新しいヒルベルト空間の定理の証明を考えたときに
>既存のMathlibで十分の射程内なのか
>はたまた、既存のMathlibの射程外なのか
>そういう議論も必要だってことだな
それはIUTの完全な検証としてブラックボックスのホワイトボックス化で必要になる話。つまり系3.12が形式化できた後の話。
そこまで行く前に大惨敗だから関係無い。
>これからも議論は進んでいくだろう
>それを見守る必要がある
大惨敗で終了したのでいくら見守っても無駄。