rmp3sの家の前

1年くらいで消えていく言葉の鉢植えたち

ゲーデル

incompleteness theoremを証明した彼が、無矛盾性の証明にいちばん関心をもっている。構成的という興味のある概念を提出して、すべての集合が構成的であるという公理がいろいろすばらしい結果を生むことを証明した彼が構成的でない集合の存在を信じている

(現代集合論入門 竹内外史

 

現代集合論入門 (日評数学選書)

現代集合論入門 (日評数学選書)

 

 

AGI 人工意識

AGIとか人工意識って単語を昨日初めて知ったんだけどAI全般と話がごっちゃにならなくていい単語ですね

 

このあたり読んだりしてます

MCUすげえ(仮題)

 

(ここに本文。なにがどうすごいのか説得力のある簡潔な美文で表記)

 

イーロン・マスクの動画みてたらキャラが面白くて釘付けになった。

www.ted.com

 

トニー・スタークっぽくねって話で盛り上がったんだけどそしたらキャプテン・アメリカは誰になるんだろ。ラリー・ペイジもおもろいけどちょっと違うよなあ。っていうかラリー・ペイジもキャラおもろい。改造される前のキャプテン・アメリカならいける?

 

www.ted.com

 

泥は土に還るか川に流される

 

ツイッターのツイートって時限的に消えてくれたらいいのになと思う。情報の川辺で、かなりライトな言葉のどろんこ遊びをしているわけで、遊んだあとの泥たちはせいぜい月単位では形が風化して土に還るのが自然だと思う

 

qiita.com

これが使えるかもと教わった。s.created_atあたりが作成日時っぽいみたいだけど、あとでみてみる。

 

欲を言うと、川辺にきては繰り返し遊ぶ泥んこの城とかもあるわけで、こういったホットな泥については風化が少し遅れるなんていうのもあったらいいな

 

(補記)「ちょっと大事な泥」という泥について

 

キーワードで言及数を検索してホットなキーワードを使っているツイートは残しにするとかどうかとか言われたけど、泥はキーワードたりえるのだろうか。

 

泥の中からキーワードを探してきてくれて整理整頓してゴミ出しもしてくれる優秀な執事がいたらよいかもしれない。別に優秀じゃなくてもいいんだけど、それだと勝手に捨てられたり保管されたりしてるのにムカっときそうなので、執事を3人に増やしたり5人に増やしたり10人に増やしたりするのはどうだろう。それぞれの美的センスで何を残すべきか決めてもらっていい。それで執事連で多数決で勝手に処理してくれればいい。こういうアプローチなら案外納得してしまうんじゃないかなとか思った。

 

あるいはfavやreplyによって泥の寿命が延びるというのはうまくいくだろうか。たとえばfav一個につき寿命が10日延びるとか、reply一個につき寿命が30日延びるとか。寿命というか泥が土に還る時間を、その泥をいじることで先送りにする感じなのかな比喩的には。

定理証明支援系

 

定理証明支援系というものがあるらしい

 

www.slideshare.net

 

www.slideshare.net

 

あとCoq を始めようとか