また欧州で洪水が起きて犠牲者が出てしまった。日本では「地下神殿」を含む首都圏外郭放水路が東京を守っているけれど、世界の大都市で同様の設備が建設されるのだろうか。二千億円超の設備が政治問題にならずに建設され、首都を守っているところに社会の成熟を感じる。 https://gaikaku.jp
やっと涼しくなり、秋晴れと紅葉の季節が来た…と思ったら、もう寒さが。夏時間も終わったので4時頃から空は暗くなり、暖房で室内は極度乾燥。粘膜がきつい…👃 https://image.nostr.build/0be748b1cd4132d9ab62ccdf41cf500879490691525fd793775b034fe12a2386.jpg
目と鼻の先だったけれど、プラハ内で引越し完了。💦 前の住居は浴槽付き物件だったので、毎晩の如く湯に浸かっていた。🛁 便器の上に置いた端末で動画を見ながら温浴をする細やかな幸せ。😇
昔のテレビCMで使われた「２４時間戦えますか」という働き方を雇用者から迫られるのは辛いけれど、週７日２４時間いつでも好きなだけ働きたい時に働けない職場というのも不便ではある。🙄
先日まで使用していた洗濯機は故障していたらしい。半分だけ溶けた洗剤が服に残っていたり、濡れてさえいない服があった。遂に服が臭くなったので、コインランドリーに持って行き９０度で洗った。生地は痛んだけれど、臭いは消えたかな。👔
一昨日の夜は停電で日没と共に真っ暗だった。 お陰で早くに眠たくなったので、健康には良かったかも。😪 今回は１〜２ヶ月で３度目の電気系の異常。全ては同じ地区の別の建造物で起きたけれど、共通の原因があるのだろうか。💡
話題のFelo.aiを使い始めてみた。無料版を使用しているが、僕の利用法では、有料版のChatGPTやPerplexity.aiと比べても遜色ない回答が得られると感じている。初めはMind Map作成が得意なツールだと思っていたけれど、実際にはMind Mapなしでも非常に役立つ回答が多いことに驚いている。 😀
日本に帰国する度に支払い方法の多様化とポイント活動の複雑さに戸惑っていたけれど、チェコも大変なことになってきている。 スクリーンショットはDATARTから。 https://image.nostr.build/950678b4c1df1fbab849916f07f9b375e4fd8c03b1b8058020d2d8aa399f2dc9.jpg
持ち家賃貸論争：英国編 https://kaeru-umi.hatenablog.jp/entry/2024/10/21/010520
ぱっと見でお手洗いの位置が分かりますか。🤔 しばらく探したら、写真の左奥にありました。🚽 https://image.nostr.build/fa4a4b82a4845f4059a470831094498ed3719cc8e475552909a653b459cd66b8.jpg
Mapifyを使ってウェブサイトに過去論文の要約を追加しました。 期待上回るまとまり具合。 Isabelle/HOLに関する私のプロジェクトの要約例はこちらです： https://yutakang.github.io/projects/faster-smarter-induction-for-isabellehol/ 皆さんは研究を要約するのにAIツールを使っていますか？ https://image.nostr.build/b44296f27cbc2a00ca147b1f238e919ce2da61f5ea91a3e8f0a3db1635e8f9de.png https://image.nostr.build/1c82868cb55ee31f683b419812702d2b6b6c2243b6c27432c02c595733864aa9.png https://image.nostr.build/00765a2e0f3dcefa5b27ad45c4533f2899a86ae41e9fa5151f9516e4157be885.png https://image.nostr.build/1d62d00e78b56be193158b7cdaa465ecf63d3290e33bc784c5a9162a8a8083b0.png
ウェブサイトを更新し、今までの研究結果の依存関係を示すグラフを追加しました。 https://yutakang.github.io/research/ まだ書き途中の部分もあるので、研究計画を終えて分かった、各手法の長所と短所についての洞察を加える予定です。🤗
雨が続くなぁ…と思ったら、中欧で洪水被害が続出。 先日まで利用していた宿の一帯は低地にあり、2002年の洪水で被害を受けたらしい。チェコでは経済被害に加え、死者も出てしまった模様。😢 https://praguemorning.cz/heres-how-you-can-help-victims-of-the-floods-in-czechia/
体感だけど、チェコでJCBカードが使えるお店が増えた気がする。2019年と2024年で大きな差を感じる。 AmericanExpress不可のスーパーでもJCBは使えたりする。使用可能なカードとして明示されているので、宣伝効果もありそう。
Coqpilotを参考に、PSLのレポジトリにもデモGIFを追加。 3Mと重いのが玉に瑕だけど、Abduction Proverの動作が一目瞭然になった気がする。 https://github.com/data61/PSL #PSL #デモ動画 #AbductionProver https://image.nostr.build/2c05845a13e303c0893c9464693d96b1855cdab64fbeb68c09a1a6de4af7b5c0.gif
フランス🇫🇷で開催されたAITP 2024に参加し、IsabelleのためのAbduction Proverについて発表しました。 私の発表では、次の3つのポイントを伝えました： 1️⃣ 推論規則「肯定的帰結（Modus Ponens）」を用いた補題の誘導 2️⃣ 仮説形成としてのタクティクス 3️⃣ 木探索からグラフ展開への移行 スライドはこちらからご覧いただけます: https://drive.google.com/file/d/1a_668KQODrTsEyAEUiyoORKO_NZTMdDu/view?usp=share_link ところで、アメリカ🇺🇸のカーネギーメロン大学の研究室がディープラーニングプロジェクトにTIPベンチマークを採用したことを知りました。TIPユーザーグループを拡大したスウェーデン🇸🇪のMoa Johansson教授とTIPチームにお祝い申し上げます！🥳 http://tip-org.github.io AITPが終わり、ケンブリッジ🇬🇧、東京🇯🇵、シンガポール🇸🇬、ナンシー🇫🇷、クタイシ🇬🇪、ドレスデン🇩🇪、プラハ🇨🇿、ボン🇩🇪、そしてオソワ🇫🇷と、移動に忙しい夏が幕を閉じました。😮💨 これでやっと研究に集中できます。😎
西ドイツの元首都ボンでTrimester Program: Prospect of Formal Mathematicsに参加してきました。🇩🇪 発表はYouTubeにあげられています：https://www.youtube.com/watch?v=9AlqFnc8QTY 発表資料はこちらから：https://drive.google.com/file/d/12Rm13_UGlXTOCy2NRpWQd1GS5miCF28x/view?usp=sharing
今まで深く考えずにAmazonでKindle用の漫画を買っていたけれど、まんが王国等の日本のサイトで購入すれば３０％引き程度の価格で購入出来たのかぁ。 実際の値引率は時期やポイント購入量にもよるけれど、多くの場合でAmazonで買うよりは安上がりになりそう。👍
Damusでの初めての投稿です！この分散型プラットフォームに参加し、技術分野の皆さんと繋がることを楽しみにしています。定理証明を支援するための人工知能に取り組んでおり、特にプログラミング言語とハードウェアの検証に興味を持っています。ここで有意義な議論や協力を期待しています。🚀
Oddbean new post about login | logout
Notes by 2155ae90 | export