Home | Notifications | New Note | Local | Federated | Search | Logout
Federated Timeline
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:01:11)
ACL2をヒューリスティックから型理論に昇華したもののような気がしてきた。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:57:09)
Cubical Agda、もしかしてACL2で身につけた感覚がとても役に立つものなのでは…？
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 20:38:07)
体調が悪すぎる
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:27:22)
guixとnixの両方が入ったFedoraになってしまうな。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:26:54)
1labのためにnixのインストールが必要らしく流石にこれは自宅で実行したほうがよさそうな感じだな。。。
ずいぞう☕🦜:skeb_logo:@zuizo@misskey.design (2026-01-06 20:09:47)
近くにおいしい食べ物屋もたくさんあることだし
#ごぞんじゲーム部 #一次創作 #漫画
---Attachments---
https://file.misskey.design/post/ef214efe-78e9-4055-a232-8c2abc79b843.webp
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:08:37)
1labのドキュメントを読んでいくのが良さそうな雰囲気らしい
https://1lab.dev/
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 19:40:39)
これからはCubical Agdaの学習に集中したいと思う。学習する価値が極めて高い気がする。
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 19:16:09)
OSC大阪について考えている
Rikuoh Tsujitani@riq0h@letter.mystech.ink (2026-01-06 18:08:53)
疲れすぎてしもつかれになった。
Reply to @tak4
たかし@tak4 (2026-01-06 17:44:49)
bibisもサブディレクトリに入れれば良かった。
その場合、bibi.i2p/forum/ みたいなurlになる。
Reply to @tak4
たかし@tak4 (2026-01-06 17:36:29)
ホストは物理的に一台、デーモンもopenbsdのhttpdが動いてゐるだけ。
bibiはウチのhttpdの愛称といふことにすればいい。
たかし@tak4 (2026-01-06 17:30:16)
サイトのurlはホスト名をbibiにして bibi. なんとか . tld にすればよかった。
変更する予定はないけど、moeドメインを手放す事情ができたら、さうする。
Shorty(デジタルかめランド)@shorty@fedibird.com (2026-01-06 17:13:50)
静的ページ、ローカルPCでサクサク編集できるの気楽でいいよね。本番環境いじるまで無限にシミュレーションできる
おもちゃの感覚で自サイトいじってる
Reply to @tak4
たかし@tak4 (2026-01-06 16:50:00)
トラッキングURLブロック機能はオフにした方が楽。
あとデフォルトで広告ブロック用のhosts.txtを読み込むのは人によっては嫌かも。
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 15:36:23)
なにかしててもしんどいし何もしてなくてもしんどい
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 14:32:56)
Cubical Agdaに取り組むべきであるという根拠がまた増えてしまった感…
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 14:13:45)
数学基礎論と物理学を組み合わせる研究はすでに進んでいて、小澤正直教授によって劇的に進展していたということを知った。数学基礎論って物理学にも応用されてたのか。。。
Coro@Coro@mstdn.maud.io boosted:
@hswugbhxwsz@best-friends.chat (2026-01-06 12:44:21)
【悲報】母親のスマホ、マカフィーとノートンを携帯ショップで同時契約していた事が発覚
なおAdblockerも契約していたがこれら全てインストールされていただけで有効化されていない模様
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 13:48:20)
昔BitZeny掘ってたっけなあ…懐かしい
Ubuntu@hswugbhxwsz@best-friends.chat (2026-01-06 12:44:21)
【悲報】母親のスマホ、マカフィーとノートンを携帯ショップで同時契約していた事が発覚
なおAdblockerも契約していたがこれら全てインストールされていただけで有効化されていない模様
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 12:34:01)
飯を食べないといけないんだけども
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 12:29:41)
うーんと、飯が食べたいな
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 12:13:26)
人間が下手
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 12:07:08)
なにやってもしんどい日あるよね
たかし@tak4 (2026-01-06 11:41:47)
AndroidでTinyAPを利用するにはFOSS Browserが快適。
デフォルト設定でも充分使へる。
黒テーマだとTinyAPも黒くなる。
ツールバーがコンパクトで画面下部にあるのでTinyAPだけが視界に入る。
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 10:38:56)
怖いなあ
もちもちずきん🍆@Yohei_Zuho@mstdn.y-zu.org (2026-01-06 10:20:12)
でかいでかい
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 09:30:49)
AgdaとACL2を趣味で触っていた結果、数学基礎論的な思想に間接的に触れることになり、物理学の統一理論が「存在する」ということについての非自明性に気づくように導かれた感じがある。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 08:49:06)
そもそも数学的に両立可能なのか疑問に思い始めてから、子供の頃からなんとなくあった統一理論への憧れ、超ひも理論への興味みたいなことが急速に崩れていくような感覚がある。同時に自分にはプラグマティズム的な感覚もあって、そもそも観測できない領域について論じる物理学って本当に必要なのだろうかということも考え始めるようになっていっている…
Older Notes