卵膜って皮なめしの要領で鞣してみると極薄の割に丈夫で、半透明で面白い素材かも。
しかも薄いのですぐ浸透して一瞬で作れる。
小さくて曲がり癖があるのはどうしょうもないが…。

コラーゲン繊維が絡まってできているものなら何でも鞣せるのではないだろうか

軟骨やアキレス腱も鞣せるのだろうか…？？

@rappi 触り心地が結構良いので、包んだり巻き付けたり貼り付けたり組み合わせたりして繋げて触れるものを使ってみても良さそう

謎の音素材（録音した）

座布団ぶったたいたこっちの音は使えそう（何にだろう？）

開き直ってIsabelleの勉強をしている
https://qiita.com/__yuriha/private/30d2b2e98a675ff60719

具体例のレベルまで詰めて考えていないので誤りやミスリーディングな記述が多分に含まれていると思われる

「手を動かして、答えを出してもわからない」「考えると、分かっていたと思ったものがわからなくなる」という状態から脱却するのはなかなか難しいものですね。

2 \mathbb{Z} が加法逆元について閉じているという程度のことが自動で証明できない…。うーむ…。

theory Scratch
  imports Main
begin
definition Z :: "int set"
  where "Z = {x. True}"

definition twoZ :: "int set"
  where "twoZ = {x. ∃k. x = 2 * k}"

lemma twoZ_closed:
  "x ∈ twoZ ⟶ (∃y. y = -x ∧ y ∈ twoZ)"
proof
  fix k
  assume "k ∈ twoZ"
  then obtain a where "k = 2 * a"
    by (auto simp: twoZ_def)
  then obtain m where "m = 2 * (-a)"
    by (auto)
  then have "m = 2 * (-a)"
    by simp
  then have "∃k. m = 2 * k"
    by simp
  then have "m ∈ {x. ∃k. x = 2* k}"
    by simp
  then have "m ∈ twoZ"
    by (auto simp:twoZ_def)
  also have "m = -k"
    by (simp add: ‹k = 2 * a› ‹m = 2 * - a›)
  then have "m = -k ∧ m ∈ twoZ"
    using calculation by auto
  then show "∃y. (y = -k) ∧ (y ∈ twoZ)"
    by auto
qed

（思っていたよりタイムラインの表示スペースを取ってしまった…）

@xiupos@mk.xiupos.net 奮闘せよ！の意味なのだろうか…。

6. 私からの最高の誉め言葉
意外とおもろいやん
7. 好きな童謡や民謡
うーん困ったな…（自分で作っておいて何だ）
春の小川、情景そのままで、歌いやすいですよね。
8. おとぎ話の主人公になるなら誰？
浦島太郎 前半のいいことした下りと、なんか遊び呆けてしまう後半が人間らしくていいですね
9. カフェを開くとしたら置きたいインテリア
黒っぽい木材の床に暗めの電球色照明にして、金属の馬とか置く
10. 好きな漫画やアニメ
アニメ映画とか含んでいいのかな（自分で作っておいて何だ）
狼と香辛料・電脳コイル・氷菓・軍曹ケロロ・攻殻機動隊・ペンギンハイウェイ

RE: https://misskey-square.net/notes/9n40d9uycq

@n1lsqn そうですそうです！

@renem2185@mi.tsujigoya.net くだらない質問ばっかりしやがって！と怒り出すChatGPTさん（リソースの浪費に関するアラーム）

@renem2185@mi.tsujigoya.net メタ的観点が混入した妙な怒り方をしそうですねｗ

@Otomu1030 設定→プロフィール→高度な設定→Botとして設定がオンになっているという意味です。Botの設定は機械による自動的な投稿を自己申告するためのものですので、あなたが人工知能ではなく人間である場合は、設定をオフにしてください。（Botがオンになっている場合、不利な扱いをされる可能性があります）

@askyq@kmy.blue Sharkeyも開発者チームの運営するサーバーがtransfem.socialだからそうかもしれません

@otail@iwshkey.com

1) ルールを表記する数式にコストを割り当て、コストの大きさを複雑性と定義する。（例: cost(n) = \log (2+|n|), cost(a_k) = \log (2+|k|), cost(X + Y) = cost(X) + cost(Y) + 1, cost(a_{f(n)}) = 2 cost(f(n)) などなど

2) nを入力し、a_nを出力するチューリングマシンのプログラムの長さを複雑性と定義する。（万能チューリングマシンの実装や、入出力のインタフェースは適宜与える）