戻る

[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.

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

> 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 とはてブを見る限りでは誘発していた)

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