26/07/29 15:12:08.80 4XyltZAE.net
>>617
>＞１）Lean語の方に何か追加するか
>新たな公理の追加はＮＧ
>これわかんないやつは素人
下記のヒルベルト空間の例が合っているかどうか だが
有限次元の線形空間を Leanで扱えるようにはなっても
当然だが、無限次元は扱えない
だから、例えば 無限次元ヒルベルト空間を扱うための
Mathlib を整備すれば、その整備されたMathlibの範囲において
無限次元ヒルベルト空間が扱えるってことだね
これを、望月IUTにおいてみるに、まずIUT以外での
確立された遠アーベルMathlib の整備が必要だね
そして
その上で、今回のLANA中間報告のLean語でのコンピュータ証明の位置づけが問題だが
上記ヒルベルトで言えば 新しいヒルベルト空間の定理の証明を考えたときに
既存のMathlibで十分の射程内なのか
はたまた、既存のMathlibの射程外なのか
そういう議論も必要だってことだな
これからも議論は進んでいくだろう
それを見守る必要がある
(google検索)
数学 証明 Leanで 無限次元ヒルベルト空間は扱えますか？
AI による概要
Leanで無限次元ヒルベルト空間は十分に扱えます。公式数学ライブラリであるMathlibには、内積空間、バナッハ空間、およびヒルベルト空間（完全内積空間）の一般的な理論が定義されています。
URLﾘﾝｸ(arxiv.org)
arXiv:2602.17064v1 [math.OC] 19 Feb 2026
Formalization of Two Fixed-Point Algorithms in Hilbert Spaces
Leanにおけるヒルベルト空間の仕組み
・型クラス（Typeclass）による表現: 任意の型 \(H\) に対して「内積空間（Inner Product Space）」の構造と「完備性（CompleteSpace）」の性質を課すことで、次元の有限・無限を問わない抽象的なヒルベルト空間を記述します。
・具体的な無限次元空間: \(L^{2}\) 空間や二乗総和可能な実数/複素数の無限列空間（\(\ell ^{2}\) 空間、lp）などが定義されています。
略す