LEANも数学もよくわからんなぁ

微分形式の幾何学を勉強し始めた。 位相空間論も解析学もちゃんと理解できていないのに大丈夫なのだろうか。 案の定、自分で書いた証明が正しいのか判定することすらできず、周りに聞ける人もいないのでLEANで証明を書きたくなった。 人間のチェックなんて信用できない。まして自分のチェックをや。

ところが、LEANのライブラリは当然そんなに充実していなくて位相やら微分やらの定義から自分でやる必要がありそう。 それに、LEAN標準ライブラリの集合はどんな集合論に基づいているのかよくわからなくて困る。 Reference manualの標準ライブラリの章を早く書いて欲しい。

あと、もっと基本的なこととして、 のとき、 とからを導くのが難しい。 友人曰く、これはη変換に関係があるらしい。 勉強することが多くて楽しい。