#知らぬ間に椅子の上で気絶部

2時間と少しくらいか

このアカウントは、notestockで公開設定になっていません。

Fahrenheight ←→ Celswidth

洋式便器にクソデカうんちをドロップするとき、脳裏では巨大隕石が地球に衝突して大変なことになるときの BGM が流れている

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

横行情報は独自取材部分だからね (?)

なんだこれ(ら)、私が流し読みした解釈と全然違うんだが

[2405.10387] Grothendieck's use of equality
https://arxiv.org/abs/2405.10387

仕方ないのでもう少しちゃんと流し読みしてる (?)

equality (等価性) ってやつは思ったほど明らかな概念でもなくて、それゆえ割とファジーに使われていて定理証明支援などに乗せようとしたときその曖昧さが明らかになってしまっている、というのがまず件のペーパーの言わんとしているところよね

具体例パートだと思ったところに結構重要なこと書いてあって、全部読まにゃ駄目か……？ となっている (めんどくせえ)

本当は性質について "universal property" を考えるべきなのに何らかの具体的なモデルの上で考えてしまうせいで、より一般化された強い言明をしたいとき証明を弄るのがダルいという感じか

で、具体的なモデルの上で考えるとき同型のような概念が結構使われているんだけど、それが "universal property" 上でいえることなのか具体的なモデルで考えているからこそいえることなのかを区別したくないとき equality symbol を abuse するトリックが使われると。
論文タイトルの "Grothendieck's use of equality" はまさにグロタンディークがやってみせたこの用法のことを言っているわけか。タイトル回収。

それが1つめの穴で、もうひとつの穴としては (具体例パートだったので読み飛ばしたけど) canonical な写像を考えるとき暗黙に符号を決めているような例が指摘されている。
著者が書かなかった暗黙の慣習があることを指摘するのは難しくないが厳密に考えたい人 (定理証明支援系含む) にとっては不必要に物事を面倒にする原因になっていると。

1つめの穴のような話は advanced mathematics をやるときほど雑に踏まれる傾向があるので、今後 modern mathematics の形式化などに踏み出すにつれ、このような事例はもっと多く出てくることになるでしょう、ということで締められている。

ほなここから感想タイム

数学の「＝」（等しい）とはどういうことか？　英ICL教授が発表　「コンピュータの登場で定義が曖昧に」：Innovative Tech - ITmedia NEWS
https://www.itmedia.co.jp/news/articles/2406/10/news058.html

この記事で一番引っ掛かっているのは記事タイトルに足された「コンピュータの登場で定義が曖昧に」という部分で、元論文は advanced / modern mathematics で特に曖昧にされがちという話はしているが「コンピュータの登場で定義が曖昧に」なったなどという話はしてないはず。
定理証明支援に落とそうとすることで、もともと含まれていたそういった曖昧さが露呈した、という話だったように原文は読める。

> 一方で、論文著者であるバザードさんは、将来的には、コンピュータ証明の数学ライブラリが充実することで、数学者が等号の厳密な意味を気にせずに済むようになるかもしれないという。数学者がよく分からず直感的な等号の使い方をしたとしても、システムが理解して不備を指摘してくれるようになるからである。

これも文面的には間違っていないけど何か引っ掛かる要約なんだよなぁ

> Once the systems are this mature,

コンピュータツールが進歩して紙の上で論ずるのと同じくらい簡単にコンピュータ上で定理証明をできるようになれば、

> it might be the case that future generations of mathematicians will not have to worry about what people like Grothendieck mean by equality,

将来の数学者はグロタンディークのような人々が equality というとき何を意味していたのかに煩わされる (have to worry about) ことはなくなるかもしれない、

> because the systems will allow us to use the concept the way that it is currently used by mathematicians in practice.

ツールによって、数学者が現状やっているように (曖昧に) この概念も使えるようになっているだろうから。

で、 hakaiya のふんわり解説の方は ITmedia NEWS の方をベースに何か言ってそうなうえ「『写像』を理解できない人のため」レベルのふんわりふんわりファジーな話しかしていないので、そもそも論文を読むときに参考にするレベルの話はしていないし理解の助けになるものとして挙げるべきではないと感じました

グワー、スレッドが切れてる

> They will also point out to the author

また、そういったシステム (ツール) は数学者に指摘してくれるだろう、

> cases when it turns out that they didn’t fully perceive what they were doing

(数学者) 自身が何をしようとしているか完全に理解していないことが判明した場合には。

> (by pointing out possibly nontrivial issues which need to be resolved in order to make an argument complete).

議論を完全にするために解決が必要な非自明な課題を指摘することによって。

……というわけで、「厳密な意味を気にせずに済む」とは言ってないと思うし (have to worry about の訳のニュアンスの問題？)、「よく分からず直感的な等号の使い方をしたとしても」というのもそれ自体は間違ってはいないけど元論文ではふんわりともう少し一般化した話も含めて書いているようにも読める。特に結論まで確認した後では。

> バザードさんは「コンピュータ支援による形式化が進むことで、数学における等号の概念的問題が解消される可能性がある」と見通している。

これも間違ったことは何も書いていないけど、日本語でこの記事にこう書くと、ぼんやりと勘違いされそうな感じだなぁという……

> However, over the last few years myself and hundreds of other mathematicians in the Lean community have spent many many thousands of person-hours building a digitised library mathlib ([mC20]) of standard undergraduate, Masters and early PhD level mathematics, so this is going to change.

ここ数年で私含め Lean コミュニティの何百人もの数学者がものすごい労力をかけて学部・修士・博士レベルの数学の形式化 (定理証明支援系のライブラリ実装) を行ってきたので、こういった (問題のある) 状況も変わっていくだろう。

> I hope that before I die, these computer tools will have matured to the extent that it is as easy to do mathematics in them as it is to currently do it on paper.

私が死ぬより前には、コンピュータツールが進歩して紙の上で論ずるのと同じくらい簡単にコンピュータ上で定理証明をできるようになっているといいんだけど。

……というわけで、「人々が (曖昧な用法などを踏みながらも頑張って解消して) 定理証明支援系の上での形式化を進めていくことで状況は変化してきている」ということを踏まえたうえで「ワイが死ぬまでに良くなってるといいな (望みがないわけではない)」くらいのことを言っているように読めるので、「『〜解消される可能性がある』と見通している」とまで言われると、いやそこまで強い未来予想はしてないよね？ という気持ちに。
(ワイの英語力の問題なのか？)

で、以上のことを踏まえたうえでﾁｭｲｯﾃとはてブをぼんやり眺めているが、たまーにちゃんと解釈してそうな人はいるものの総合的には頓珍漢なことしか言ってないようなコメントばかりなので、「違和感持ったら原文読もうよ」とかのレベルではなく「せめて overview か summary は読もうよ」くらいの小並感になってしまった。やはり品質検査されていない群集の言葉なんてアテにするもんじゃないね

というかそもそもタイトルは equality のこと言ってるけど論文の本題って equality の曖昧さを含めてもうちょっと根っこの部分にある問題の分析な気がするし、 ITmedia NEWS の記事の徹頭徹尾等号の曖昧さだけが問題であるかのような書きぶりはちょっと誤解を誘発する (というか実際 Twitter とはてブを見る限りでは誘発していた)

RT/fav した人には申し訳ないが、これはちょっとスレッド切れてると良くないなと思ったので削除して繋げて再投稿しました

このアカウントは、notestockで公開設定になっていません。

「ソースコードを自分でも読めそうなものを優先して使おう」という発想自体が既にだいぶ少数らしいということには以前から気付いていたので、むべなるかな

inotify みたいなドライヤーが着弾した

@hadsn まず in_reply_to 的なリプライ先メタデータを web UI から編集できる気がしなかった (私が見落としているだけで実はできる可能性はある) ので……

@hadsn もしかして虚空から生やしてしまったツリーを消さずに取っておけという話でしたか。
(「ツリーに繋げ直したトゥートのパーマネントURLに差し替えれば」の意味がとれませんでした……)

古い投稿を削除したのは、他ならぬ言及対象が「元論文の一部のみに限って言及することで誤解を招いている」というのと更に「その言及の一部のみを読んで勘違いしている人々」まで見えていたので、この文脈で万が一にも二の轍を踏みたくないと考えて全てを単一スレッドに収めることを優先した形です

時限ミュートはリアルタイム実況系コンテンツにのみ使いがち (まあ実況はだいたいハッシュタグとか固定キーワード付けてくれるほど行儀良くないことがほとんどだが……)

典型的にはアニメとか新製品発表会とかの配信

リアルタイム実況以外の時事言及とかはそもそもミュート困難だったり言及が続くことが多いので、興味ない話ばかりだったらミュートを頑張るより TL を離れることにしている

脳卒中  |  Android Developers https://developer.android.com/training/wearables/wff/group/part/draw/style/stroke?hl=ja

記事を開く前から笑わせにくるのやめろw

結局 ITmedia NEWS の記事は端的に何が問題だったのか考えていたが、正しく理解するのに前提知識が必要なレベルの話を、大事なことへの言及を避けて表面的にさらった点と、それを読みやすくしたうえで、理解できると思われるような読者層でない人々に向けて提示したという2点が問題かなという結論

解説されている問題の本質を示さずさらっと表面的に撫でているのに、ちゃんと読みやすく解釈できる文章にしてしまっているせいで、読者は重要な情報を全然受け取れていないのに何かをわかった気になれてしまう。

むしろ前提知識がほしいレベルの本質情報を隠したからこそ、人々がわかった気になれるのかもしれないけど。
それがメディアとして望ましい振る舞いだとは思えない

作文能力が悪い方向に発揮されとるんよ

べつにわかりやすく説明したくてしたわけではなく、「テキトー言ってんじゃねえ」にエビデンスを付けただけなので……
「わからんなら言及せず黙っとけ」の見放すスタンスは変わってないです

件の記事はまさに「不正確でもいいからわかりやすく」を地で行くもので、そしてﾁｭｲｯﾃやはてブで見られた頓珍漢なリアクションはその有害性をこれ以上なく明確に示しているように思われる

もちろん前提知識含め本質に手が届くところまで突き進むつもりのある人なら「始めは雑でもガイドラインがあれば……」となるかもしれないが、ではここで聞きますが、そのへんのランダムなネット記事を読んで「本質に手が届くまで前提知識含めちゃんと学習するぞ！」となる人の割合は如何ほどでしょうね

結局のところ、気合の入った学習者相手にはそれなりの向き合い方が、そしてそうでない通りすがりの人相手にもそれなりの向き合い方がそれぞれある、そしてそれらの方法論には少なくとも十分な互換性はないことが多い、そういう話だと思っている

いくらわかりやすく説明しようと、読まなきゃ理解されないし、そして読まれないんですよ

「わかりやすく」に加えて実用上は「学習する気のない人が読むのをやめない文字数で」という制約がある、と考えるべき

https://mastodon.cardina1.red/@lo48576/113439526095863506

だからこそ、その気のある学習者とそうでない人を相手に方法を (そして踏み込み具合を) 変えないといけない

そしてこのご時世、ｲﾝﾀﾈｯﾂでの物書きはそれに加えて「途中で聞く/読むのをやめた人が勘違いしたうえそれを吹聴したりテキトーなことをするリスク」まで含めて行動を決める必要があるわけで、やってらんないわね

時間制限と労力制限と文字数制限と打ち切りによる異常状態を考慮しなくていいなら、テキスト積み上げてわかるまで真摯に説明すりゃいいんですよ。文字で積み上げる文明はそれができる

そして学校教育も (程度の差はあれ) 概ねこれをやっている

元論文のリンクがあるのに大半の人は読まないわけで、じゃあ少しマシな説明を日本語で与えたところでそれが読まれると信ずる理由もべつにないですよね (あれは「英語だから読んでいない」だけではないと思うので)

間違った理解をしたくなくて仕方ない、自分の誤解をただすためならコストを支払うことも厭わない、みたいな人にしか “指摘” は読まれない。

いないわけではないけど、人々の標準がそういうタイプだとは思えないし期待もしていない

「さあ、はじまるザマスよ!」
「進行するでガンス！」
「因果(インガ)ー」

「論文」を読まない理由やメカニズムはそのまま「論文でない任意の (一部の人々にとっては “簡単” な) 文章」に流用できるのではという話です

で、「難しいから読まれないが、もう少し簡単にすればあるいは」の無限退行が止まるタイミングは人それぞれだが、十分に高い可能性として「最初に目にした文章で、そのうちのさらにスルッと受け取れなくなるまでの冒頭部分だけ」になっている場合を想定しています。悲しいことに。

読み解き方を説明しようが、それが実効性を発揮して誤りを解消する段階まで到達できなければ事態をかき乱すだけにもなりかねないし、そういう状態になった人々にまで責任持ちたくないし関連付けもされたくないですよ。そんな余裕ないので。

なので私は真面目な話を「読んでくれ」のスタンスで書くことはあまりなくて、基本的に「わかるやつには有益だろ、わからんやつに接待するつもりはないから出直すか諦めろ」というやるだけやって突き放すスタンスで書きがち

本当は「わかってない人が『今オレ全然わかってない……』とはっきり自覚できるような文章」を書けると良いなとも思っているが、さすがに特殊な訓練が必要そうだしうまくやれる気はしないですね。特に専門用語と日常語彙が競合している場合などは。

わかりやすい説明を残すことは否定しないけど、その作業は結局公共への奉仕のコストとして計上するようなものになりがちなので、余裕のある人が余暇でやるか、誰かが個人的に報酬を出すかでもないと厳しいだろうと思いますね。
有用なのはわかっているが、その活動に持続性を持たせるのがコスト的に難しい。

本質的には「すべての外国語文献に日本語訳があればいいのに」と言ってるようなもんですよね。

直接読める人はわざわざ訳を残しても自分へのメリットが薄く、そのうえ訳を誤読する人がいたら (訳自体に問題がなく読者が全面的に悪くとも) 責を負いかねない立場に身を置くことになる。
そして直接読めない人はそもそも翻訳できない。

そのうえで、たとえば誤訳が広く共有されてしまったとして、指摘をどこかに置いておくだけなら通常の翻訳コストくらいで済むけど、それを元の誤訳と同程度に広く共有するコストなんて誰が払えるんですかと。しかも初出の誤訳の方が基本的には広まりやすいのに。

さてここで翻訳コストが必要なくなる妙手がありまして、何だかわかりますか。

直接読める人しか相手にしないことです。

裾野がどうとか母語で思考できる方がどうとか、いろいろ論点はあるんだけど、少なくともこれをエリート主義的だとして一蹴するのは言うだけなら簡単だが、じゃあ実際それを避けるための “翻訳” コストを払い続ける (あるいは払う気のない人に押し付けられてフリーライドされ続ける) ことに界隈の人々が耐えられるんですかという。

結局リソースの問題なんだよね。

情報を集める労力を出せないから。
情報を理解する思考リソースと学習を捻出でいないから。
自分で使えない情報を出す余裕がないから。
わからないことをわからないと認めることによる不都合を補填しきれないから。

そういうリソースのなさ由来の問題を「でもリソース出せば解決するでしょ！」とするのはあまりに無意味な正論

認知や思考のリソースや時間や体力について、トレードオフの問題と向き合わないといけない。こういうまとめ方は「要はバランスおじさん」みたいで嫌なのだが。

そういう諸々と、身を削らない範囲で誠実に向き合おうとすると、結局「趣味の範囲でやってやるがオメーのケアはするつもりない、ケアが必要なら自分でやれ、それが無理なら最初からこっち来んな」くらいのスタンスに落ち着くわけです。文脈次第で多少のふれ幅はあるけど。

解説や指摘を書いたって良いが、そのために削られた私の睡眠時間は誰も補填してくれない。だから趣味の外の範囲でやりたくないし、やろうとしてはいけない (自衛のために)。

言わんとすることはわかるけど、それで弱い部分 (世間による誤解に耐えられない性格や立場の人々) に力をかけ続けるくらいなら、最初からそういう有象無象の戯言を無視できるような業界構造を作る方がまだ人道的で健全なんじゃないかと思うことはある。
もちろん完全な遮断は腐敗を生むので風通しは必要だしそのバランスは難しいけど。

もちろん何らかのうまい構造でそういった公益性の高い活動に適切な報酬が出るようになればそれが良いのだろうけど……そんな報酬どこから出るねんという話と、報酬が出る仕組みは必ずハックされて当初の目的を果たさない形での搾取が始まるという話があるので、そううまい解決策はない

事実、ページビューや付随する金銭報酬という形で情報発信に報酬が出るようにしたことで、テキトー解説がブランド力をもって巷に発信されまくるようになったわけですよね (いつぞやの医療系情報サイトの話を例に出しても良い)

教科書を書く人もいれば大嘘で本を書く人もいて、だいたいにおいて後者の方が儲かるし社会全体でのネームバリューも得られるわけです。
まともに戦えばそれだけ不利になる。

つまりそれが情報発信自体を趣味でやっているということです

趣味でやってる人が全部やってくれるなら私も自分の趣味に没頭できるのだが、残念ながらそうでもないので私が †指摘† を書くハメになったわけですね。今回は。

楽しくもないのに。

趣味で読むなら「この記述勘違いされてそうだけど原文のどこにあるんだ？」みたいなカスの邪念なしで好奇心だけで読みます

まあゴミ拾いボランティアみたいなものだと思って手を出すことはあるけど、ため息つきまくりですよ。ゴミ拾いもボランティアも趣味としていないので。

陰キャオタクのなけなしの社会性の発露だと思ってください

バグ修正やパッチにはちょっとした名誉という報酬があるかもしれないが、誤情報の修正は名誉ポイントまじで全然貯まらないよね。バグ修正とかバグ指摘とは比較にならないくらい。

ネットミームとはいうが、べつにそれらも著者のものであってｲﾝﾀｰﾈｯﾂ有象無象民の持ち物では断じてないのだから、許諾とれていれば道義的に何の問題もなかろうし、そして許諾は当然取っているでしょう

ﾈｯﾂ民が与えたものなんて「注目度」とか「作品外文脈」 (悪く言えば「おもちゃ度」) みたいなもので、元の作品が元来抱えていたものではないのだから、派生先のパロなりオマージュなりがそれを当然のごとく受け継ぐべきと考える合理性は低い

まあそれはそれとして、「既存コンテンツへの注目を “スライド” する形で広告へ持ってきた挙句流出は禁止する」みたいな動きがひとりよがりに見えるのはわからんでもないが、そもそも広告ってそういうものだし……それが不満なら最初から広告コンテンツに乗っかるべきではなく冷やかに無視するべきだった。
無論それはそれでオタクコンテンツの存在感や市民権の低下に繋がるけど。カネにならないものにリソースは出されないからね。

このアカウントは、notestockで公開設定になっていません。

鉛の入ってないワイン

ｲﾝﾀﾈｯﾂとﾏｸﾖﾅﾖﾖに限って話をするなら、ﾈｯﾂの者共はﾏｸﾖの CM コンテンツを違法アップロードやら文脈汚染やらでやりたい放題の無法をやってきたわけで、ここでぶっとい釘を刺されたって自業自得だし当然のことというか、過去20年のｲﾝﾀﾈｯﾂを見てもう一度同じこと言ってみろよという感想にしかならんのよな。

日頃の行いが悪いってのはつまりこういうこと

Real Factory Automation

Gentoo は壊れづらくてコントロールの効く良い distro ですよ
常用におすすめ

最近はメジャーなアーキテクチャ向けにビルド済みバイナリパッケージも配布されるようになってきたのでビルド時間問題もかなり解消されてきている (もちろん最新 CPU とかを持ってる人は自前でビルドして性能を追求しても良い)

このアカウントは、notestockで公開設定になっていません。

「課金 (誤用)」のように alternative meaning にスイッチする接尾辞を付けることで誤魔化したりはする (「末代 (誤用)」みたいに)

継続的な支払なら「加入」が近そう

このアカウントは、notestockで公開設定になっていません。

今度から 5 Pro のことｺﾞｰﾌﾟﾛと呼ぶか (最悪)

ファックス単品に空目して「そんなことあるんだ……」と思ったが、そんなことなかった

このアカウントは、notestockで公開設定になっていません。

トラのあな (正孔)

このアカウントは、notestockで公開設定になっていません。

このアカウントは、notestockで公開設定になっていません。

ﾋﾟｯｼケース (Define 7) が届いたが置く場所がないので、またしても模様替えを検討している