数学2024arxiv.org
Grothendieck 对等式的使用
Grothendieck’s use of equality
专业 · 约 90 分钟读完前置知识：范畴论基础、类型论基础、数学基础（Lean/形式化）
导读
论文考察 Grothendieck 式的'等号用法'：数学中习惯把典范同构的对象直接视为相等（如把整数当作有理数），并探讨这种做法能否被严格论证和形式化。据评论所述，作者在 Lean 中开展工作，并对同伦类型论等非经典类型论的解决方案持保留态度。
HN 关注点：HN 读者多为类型论与形式化数学爱好者，讨论焦点是 HoTT/一价性是否已解决这一问题，以及 Lean 路线的局限。
HN 评论精选
这几条评论里：质疑 2 补充 2
质疑HoTT 本可解决论文提出的问题，但作者用 Lean 且排斥非经典类型论。
对于这个问题，同伦类型论（HoTT）给出了一个很好的答案，它处理了作者提到的所有复杂情况，这也是类型论学家当初对 HoTT 感到兴奋的原因之一。唯一的问题是作者在用 Lean，而且显然对非经典类型论不屑一顾，于是我们又回到哀叹类型论中的等号是坏掉的……（这是根据二手信息，如果说得太重请指正）
fmap查看英文原文
For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken... *) I'm going by second hand accounts here, please correct me if you think this statement is too strong.
补充这本质上是隐式类型转换，类型和转换一多，图表就可能不再交换。
这个问题大概以'隐式类型转换'的名字更为人熟知。严格来说，有理数 1 和整数 1 并不相同，我们只是有一个保持所有相关性质的转换映射。当涉及 1000 个类型和 10000 个转换映射、相关图表不再交换（即结果取决于转换顺序）时，麻烦就来了。
generationP查看英文原文
This is probably better known here under the name of implicit type conversions. Strictly speaking, the rational number 1 is not the same as the integer 1; we just have a conversion map that preserves all the relevant properties. It's all fun and games until there are 1000 types and 10000 conversion maps involved and the relevant diagrams no longer commute (i.e., it depends what order you go).
补充只要关心的性质都由泛性质导出，同构即相等，关键看你区分哪些性质。
等号在哲学上确实令人困扰，但实际重要的是'同一者的不可区分性'：如果你用到的每条性质都能从泛性质推出，那么'同构意义下相等'就等于相等。所以把魔方看作面旋转群时，所有魔方都相等、世上只有一个魔方；但如果你关心贴纸胶水的化学性质，它们就不再相等了。
juped查看英文原文
Equality can be philosophically troubling, but as a practical matter, what you care about is the indiscernibility of identicals, and if every property you use follows from a universal property, then equal up to isomorphism is just equal. So every Rubik's cube is equal considered as a group of face rotations, and there's only one Rubik's cube, but if you care about chemical properties of sticker glue, they're no longer equal.
质疑等号一词多义（定义/相等/同一/比例），论文未讨论这一点。
每当这个话题出现，我总觉得等号承载了太多含义：它可以表示定义、相等、同一、比例。为什么论文没有提到等号的这种多义状态？
nyc111查看英文原文
When this subject comes up I always think that the equality sign is loaded. It can mean, definition, equality, identity, and proportionality. How come this state of the equality sign is not mentioned in the paper?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2024Hacker News 讨论帖178 分 · 129 评
同领域还值得读
一种新的相关系数
A New Coefficient of Correlation
提出了一种新的相关性系数（由 Sourav Chatterjee 提出），能够检测变量之间任意形式（不限于线性）的相关关系，且计算简单高效，主要基于排序和距离计算。
数学2021 · 682 分 · 158 评 · 引用 1进阶 · 约 60 分钟编辑精选数学的两种文化
The Two Cultures of Mathematics (2000)
这是数学家 Timothy Gowers 于 2000 年发表的一篇随笔，他把数学研究大致分成两种文化：一类是“解题者”，热衷于攻克具体难题、发展技巧（如组合数学）；另一类是“理…
数学2009 · 307 分 · 102 评入门 · 约 35 分钟编辑精选重新定义统计显著性
Redefine statistical significance
提议将统计显著性阈值从常用的 p<0.05 收紧到 p<0.005，以降低假阳性率、缓解可重复性危机。
数学2017 · 303 分 · 114 评入门 · 约 45 分钟编辑精选统计建模：两种文化（2001）
Statistical Modeling: The Two Cultures (2001)
讨论统计学中两种建模文化：一种假设数据由某种随机模型生成，侧重推断与系数解释；另一种把数据生成机制视为未知，侧重预测精度，主张使用算法建模。
数学2015 · 254 分 · 36 评进阶 · 约 60 分钟编辑精选通信的数学理论 (1948)
A Mathematical Theory of Communication (1948)
这是香农 1948 年的经典论文《通信的数学理论》，奠定了信息论的基础。
数学2016 · 169 分 · 53 评入门 · 约 90 分钟编辑精选