Wonderland — 2026-11-03
Wonderland — 2026-11-03
速览（30 秒）
- 组合: 编译器与编程语言设计 × 形式化方法与定理证明 / 气象学与气候动力学 × 法律解释学与判例推理 / 制图学与地图投影 × 认知科学与决策偏误
- 今日火花 Top 3: #1 同一个 bug 必须在所有内核里同时存在 / #5 判决书一个字节都不会改，被推翻的是指针 / #8 用声音画的地图
- 可动手候选: #1（给校验脚本找一个异构替身）、#10（摸一遍盲道纹理的分辨极限）、#7（给项目做一次“分支式”预报）
- 值得写长文: #4（机检证明的成本曲线）、#6（路径依赖是法学和气候学的公共词）、#9（认知地图画的是预期，不是世界）
组合 A：编译器与编程语言设计 × 形式化方法与定理证明 + 如果只能用手绘/纸笔计算，不能用电子设备
本期亮点: 这一组是从上一期那张“小检查器”的卡片往下追一步：检查器小到能被人读完之后，问题就变成“谁保证这个读者和机器读的是同一件事”。纸笔这条约束把答案逼了出来——不是更聪明的算法，而是换一种方法再写一遍；再追一步，还撞上了更不体面的那半边：验证的成本曲线和手写的成本曲线是反的，于是这一组四张卡分别落在谁来读、谁来信、漏洞在哪和要花多少钱上。
💥 #1 — 同一个 bug 必须在所有内核里同时存在：把检查器写成另一种语言
方法论惊讶 9 · 具体 9 · 可行 7
2022 年 Lean 官方内核的一个大数运算 bug 让它接受了一份无效证明；同期用 Rust 从零重写的独立检查器 Nanoda 拒绝了同一份证明，官方内核不到 24 小时就修好了。de Moura 说得很直接：想钻某个内核的空子，就得同时钻所有内核的同一个空子，“那要难得多”。当验证不能靠堆算力、只能靠人一行行读时，“再写一个用不同方法写的检查器”就从奢侈变成了唯一能落地的冗余——纸笔算不动第二遍，于是第二遍必须换算法。
如果要做给你最信任的那个校验脚本找一个“异构替身”——换一种语言或换一种算法重写一遍，再故意造一个让两者结论不同的输入；这就是你项目里的 Lean Kernel Arena。
参考文献 2
- Leonardo de Moura《Who Watches the Provers?》(2026-03-16：Nanoda，一个从零用 Rust 写的完整 Lean 证明检查器，“implements the entire verification logic in under 5,000 lines of code”；2022 年大数运算 bug，官方内核接受而 Nanoda 拒绝，24 小时内修复)
- 旁证：Lean Kernel Arena（arena.lean-lang.org：把所有独立检查器放在同一套测试上跑——该被拒绝的无效证明、该被接受的有效证明、结果未定的边界情形各成一列，并按 mathlib 测试用例的耗时与内存排名；官方 Lean 计划把 nanoda、lean-inductive-models、lean4lean 一并随发行版提供）
生图提示词
一张深色工作台上并排放着两台完全不同的手工仪器：左边是黄铜齿轮与玻璃透镜，右边是竹管与铜线；两台都凑近同一颗发光的半透明小方块，方块旁摊着一张泛黄的纸和一支削好的铅笔。
💥 #2 — 形式化的尽头是一张纸：Metamath 把三个定义的可信度押在纸上的证明
文化隐喻惊讶 8 · 具体 9 · 可行 6
Metamath 的 mmj2 能自动验证绝大多数定义，但三个类定义没法自动验证——官方文档直说：必须相信 Levy 的消去性与守恒性证明，“这些证明只存在于纸上，至少在有足够复杂的定义可靠性检查器出现之前”。在“不许用电子设备”这条约束下，这个被当成缺陷的信任层反而是终极目标：一条形式化可信链的最后一环，本来就该是一叠能被人读懂的纸。
如果要做把你们团队最核心的那条不变式写成一份“纸面证明”——不许引用任何工具输出，只能引用定义与已证引理；写完自己从头再读一遍，你会立刻知道哪一步其实是在相信机器。
参考文献 3
- Metamath Proof Explorer
- set.mm 首页（“there is no simple way to verify automatically the soundness of our three class definitions. Instead, we must trust the relatively involved metamathematics of Levy’s … eliminability and conservation proofs that exist only on paper”）
- 旁证：Metamath 的 sqrt(2) 无理证明页（核心在 sqrt2irrlem：若 A/B=√2 则 A、B 皆偶）
生图提示词
一间安静的档案室，一叠手写纸页摊在木桌上，最后一页末尾没有句号，只有一枚红蜡印章与一行被反复描粗的算式。
💥 #3 — 一个证明 False 的证明，诞生于一个被打包进去的旧版算术库
装置/原型惊讶 8 · 具体 9 · 可行 7
2026 年的 Lean 内核 soundness bug 猎里，攻击者发现官方 Linux 版 Lean 打包的不是最新的 GMP v6.3.0，而是含已知 bug 的 v6.1.2，并据此构造出一份 False 的证明；2026-08-21 随 v4.33.1 一并修复。漏洞不在逻辑里，而在“用哪个算术实现”里——一个手算大数乘法的纸笔检查器，恰好绕开了整条供应链。
如果要做查一遍你机器上三个最关键依赖库的版本号，翻它们的 changelog 找 “fixed a bug that could produce wrong results”；再确认你的项目里有没有任何地方默认“这个库算大数一定对”。
参考文献 2
- Leonardo de Moura《Postmortem for the Kernel Soundness Bug Hunt》(2026-08-24：GMP v6.1.2 的已知 bug 被用来构造 False 的证明；v4.33.1 修复全部问题)
- 旁证：同一次事故还催生了另一个方向的检查器——Lean FRO 的 Joachim Breitner 做的 lean-inductive-models：它不重写内核，而是在前面加一道预处理，先用证明说明一个归纳类型连同它的 recursor 与化简规则可以由第一性原理建模，从而抓出一大类内核处理归纳类型时的实现 bug。旁证：Lean Reference Manual 中“Validating a Lean Proof”一节（如何检查潜在对抗性的提交）
生图提示词
一只巨大的透明玻璃罐里悬着一枚写着断裂符号的齿轮，罐底积着一层薄薄的老旧机油，旁边散落着版本号形状的金属片。
💥 #4 — 机检证明的成本曲线：241 页的教材变成 16 万行 Lean，只要两周
文化隐喻惊讶 8 · 具体 9 · 可行 7
arXiv:2601.03298 记录了一个自动形式化项目：从 Munkres 的《拓扑学》（241 页、7 章、39 节）出发，到 2026-01-04 已产出 16 万行形式化拓扑，其中约 13 万行集中在 2025-12-22 到 2026-01-04 的两周内，LLM 订阅成本约 100 美元；arXiv:2604.03071 则用 3 万个并行的 Claude Opus 代理，一周把一本 500 多页的研究生代数学组合教材变成 13 万行 Lean、5900 条声明。手写证明的钱花在想出那一招上，机器验证的钱花在把整本书改写成能被重放的步骤上；约束一换成不许用电子设备，这两条成本曲线就整个翻了过来——纸上想出证明几乎不要钱，纸上验证它却极贵。
如果要做拿你写过的一篇技术文章试一次：只把它的核心论证改写成可逐行核对的步骤（不许写显然），数一数你补了多少步——那个数字就是你原本替读者省掉的机器。
参考文献 3
- arXiv:2601.03298（130k Lines of Formal Topology in Two Weeks：Urysohn 引理 3k 行、Urysohn 度量化定理 2k 行）
- arXiv:2604.03071（Automatic Textbook Formalization：130K 行、5900 条 Lean 声明、一周完成）
- 旁证：10.1007/978-981-95-5096-8_5《How Hard can it be to Formalize a Proof?》（机检证明的复杂度 prohibitively high，且安全定义的写法会同时影响纸笔证明与机检证明的难度）/ 旁证：reservoir.lean-lang.org 的 Odd Order 项目（Feit–Thompson 定理的首个 Lean 形式化，此前只有 Gonthier 等 2012 年的 Coq 证明；lean-eval 曾把它列为 no Lean port 的挑战题，2026-07-16 首次被接受；项目还顺手产出了新数学——Bender–Glauberman 附录 C 的问题 1）
生图提示词
一座由十万张写着步骤的纸条垒成的巨塔，塔基摊着一本厚书，塔顶飘着一面很小的三角旗。
组合 B：气象学与气候动力学 × 法律解释学与判例推理 + 如果必须完全用 COW（copy-on-write）实现
本期亮点: 写时复制这条约束意外地把两个领域拉到了同一张桌子上：判例的正文从不被改写，被推翻的只是指针；而气候预报天生就是“一个不可改的初值 + 一堆互不干扰的分支”。更妙的是第三张卡——“路径依赖”这个词，法学和气候学共用了几十年。
💥 #5 — 判决书一个字节都不会改：被推翻的是指针，不是正文
同构惊讶 9 · 具体 9 · 可行 7
Westlaw 的 KeyCite 旗标（黄旗：存在负面引用；蓝条纹：已被上诉；被推翻、被取代、未被遵循）挂在判决原文旁边，原文一个字都不动；而 ZFS 的写时复制语义是“every write creates a new version of data rather than modifying existing blocks”，因此快照零成本。在法律里这件事有个现成的名字：stare decisis。推翻先例从来不改先例，它只是让所有指向它的新指针改指到别处——被判“死刑”的那一段文字仍然躺在原处，只是没人再往那儿指了。
如果要做拿一份你常引用的规范或 ADR 试试：给它加一个“状态指针”（有效 / 已废止 / 被取代 / 不再推荐），正文一个字不动——你会发现整套文档第一次有了不撒谎的历史。
参考文献 2
- Thomson Reuters Westlaw《Checking Cases with KeyCite》（“Different flags mean different treatments, such as being overruled, superseded, or not followed by another court”；“one identified point of law can be overruled while other points remain good law”）
- ZFS 写时复制语义（技术词条：“ZFS never overwrites data in place — every write creates a new version”，快照因此近乎零成本）
生图提示词
一块刻满抽象纹理的巨大石碑立在光柱里，石碑侧边钉着一排小铜牌，其中一枚正被取下，移向阴影里另一块更新的石碑。
💥 #6 — 路径依赖是法学和气候学的公共词：历史不是受控实验，谁也重跑不了
文化隐喻惊讶 8 · 具体 9 · 可行 6
2007 年 Michael Dorf 在 FindLaw 撰文《The Supreme Court and the Butterfly Effect》，明说“自然科学家和社会科学家都把它叫作 path dependence：初始条件的差异在足够长的时间里会放大”，并用 Bush v. Gore 举例——若法院不介入，“过去 81 个月会非常不一样”；他还提到一颗六千五百万年前撞上地球的彗星。当法学毫不忌讳地借用混沌论的词，法律就不再是“依法推理”，而是一条带初值的轨道——只是这条轨道没有人能重跑一遍。
如果要做拿你团队最重要的一个历史决策做一次“路径依赖复盘”：写下当时的初值（谁在场、缺了什么信息、当时最省事的做法是什么），再看今天哪些结果其实是那三个初值的下游。
参考文献 2
- Michael C. Dorf《The Supreme Court and the Butterfly Effect》FindLaw (2007-09-24：“Natural and social scientists refer to it as ‘path dependence’. Initial conditions make large differences over enough time”；Bush v. Gore；65 百万年前的彗星)
- 旁证：arXiv:2410.04493《When Common Law Ages》（分析 1800–2000 年四百万份判决，发现“路径突变”逐年减少，先例越来越形成惯性）
生图提示词
一条由无数微小心形沙粒组成的河流从远方来，流到岔口时分叉成两条河，两条河各自奔向两座风格迥异的城市。
💥 #7 — 预报员和法官拿着同一种结构：一个不可改的初值 + 一堆互不干扰的分支
方法论惊讶 8 · 具体 9 · 可行 7
CMIP5 实验设计要求每个核心实验至少做 3 个集合成员、tier-1 扩到 10 个，并用“2000 年代额外初值”扩展；Lorenz 的可预报性论证说，初值误差决定了预报能走多远。在写时复制的约束下，预报系统的正确形状不是“一个越来越准的模型”，而是“一个不可改的初值 + 若干条互不干扰的分支”；判例法早就在用同一形状——每个新判例都是从一份不可改的先例快照里分叉出来的一条支线，谁也不许回头改写先例。
如果要做给你最重要的一次预测做一次“集合预报”：固定同一份初值（需求文档、当时的依赖版本），跑 5 条差别很小的执行路径，统计结论会不会翻转——这就是业务版的 ensemble。
参考文献 4
- Taylor et al.《A Summary of the CMIP5 Experiment Design》（每个核心实验至少 3 个集合成员、tier-1 至少 10 个成员、用 2000s 的额外初值扩展）
- 旁证：Krishnamurthy《Predictability of Weather and Climate》(NOAA 文献库)：Lorenz (1963b) 发现两份解之间的初始微小差异会随时间长大，最终与两个随机选取状态之间的差异一样大，混沌对初值的敏感依赖对天气预报有巨大影响，并因此催生了对可预报性的量化
- 旁证：Molteni et al. (1996)《The ECMWF Ensemble Prediction System: Methodology and validation》（集合预报成为业务系统）
- 旁证：Wikipedia “Butterfly effect”（Lorenz 1972 年报告题名 “Predictability: Does the Flap of a Butterfly’s Wings in Brazil Set Off a Tornado in Texas?”，题名由 Philip Merilees 想出；Lorenz 原本用的是海鸥）
生图提示词
一个玻璃球里封着一座微缩城市，球体表面裂开成数条发光的光路，每条光路从同一个起点出发，却通向不同的远方城市。
组合 C：制图学与地图投影 × 认知科学与决策偏误 + 如果必须用纯音频/纯视觉表达，不能用文字
本期亮点: “不许用文字”这条约束把制图学逼到了它的尽头：地图本来就是视觉的，但一旦连标注、图例、地名都拿掉，剩下的只有纹理、形状和声音。于是就有了声音地图、心智地图，和城市里唯一一块没有字的地图——盲道。
💥 #8 — 用声音画的地图：把伦敦和巴塞罗那分成“混乱/单调/平静/兴奋”
装置/原型惊讶 8 · 具体 9 · 可行 7
2016 年 Royal Society Open Science 的《Chatty maps》用社交媒体上带地理标签的影像配乐库，编出第一批城市声音词典，并把伦敦、巴塞罗那的声音映射成“哪片区域混乱、单调、平静、兴奋”；后续工作把这条线推到用卫星影像、音频与文本的联合嵌入做全球声景制图。制图学的第二条轴不再是地名，而是声音——这张地图上的“地点”是靠听认出来的，投影保不住的东西，换个通道反而保住了。
如果要做录 30 天通勤路上的声音并打上定位，把每个采样点归入四类，再叠到一张普通地图上——你会得到一条只属于你的“听觉地图”。
参考文献 3
- 10.1098/rsos.150690（Royal Society Open Science 3:150690, 2016：“we were able to map which areas are chaotic, monotonous, calm and exciting”）
- arXiv:1603.07813（Chatty Maps，首个城市声音词典）
- 旁证：arXiv:2408.07050（PSM：多尺度零样本声景制图，卫星影像 + 音频 + 文本联合表示）
生图提示词
夜里的城市俯瞰图，屋顶之间浮着一圈圈半透明的声波涟漪，青色、紫色与琥珀色的波纹互相重叠，像一张用声音画的城市噪声图。
💥 #9 — 1960 年的导航机器是纸和笔：Lynch 让波士顿人凭记忆画出自己的通勤路线
文化隐喻惊讶 8 · 具体 9 · 可行 7
Edward Tolman 1948 年在《Cognitive Maps in Rats and Men》里造出认知地图这个词：他在迷津实验里发现老鼠会在预期被打脸的路口停下来犹豫（vicarious trial and error），并写下“对它们来说，自然地预期同一条空间路径总会导向同一个结果”；十年后 Kevin Lynch 让波士顿与洛杉矶的居民凭记忆画出日常路线，得到“一种符号结构，视觉-空间表征由此被检索出来”，并由此造出可意象性（imageability）这个词。地图是描述性的，认知地图却是预期性的：它画的不是世界长什么样，而是我这么走会发生什么，而且它随时能被现实证伪——一张没有文字的地图，本质是一堆等着被检验的赌注。
如果要做做一次 Lynch 式实验：让五个同事闭眼画出他们每天上班的路线，然后叠在一起——那张图就是你产品的真实导航界面。
参考文献 2
- 10.1037/h0061626（Tolman, Cognitive Maps in Rats and Men, Psychological Review 55:189-208, 1948：“it is natural to expect that the same spatial path will always lead to the same outcome”；迷津里困难路段让老鼠犹豫更多，“越笨的老鼠犹豫越多”）
- 旁证：Failed Architecture《Kevin Lynch and the GPS: Predicting the Culture of Navigation in 1960》与 Lynch, The Image of the City (1960)（“it was a symbol-structure on which mental processes operated to retrieve information”）
生图提示词
五张泛黄的手绘路线图叠在桌上，线条歪歪扭扭却都指向同一栋楼，楼顶飘着一面小旗。
💥 #10 — 盲道是城市里唯一没有文字的地图，而它最大的敌人是纹理太像
方法论惊讶 8 · 具体 9 · 可行 8
美国国家科学院 2025 年的《Tactile Wayfinding》指南点出一个很具体的麻烦：铺装纹理之间的差别如果不够明显，就 not highly recognizable——例如刷面混凝土与几乎无纹理的铺路砖；而这套标准自己也有过一段难产史：1994 年美国联邦（Access Board、DOT、DOJ）因缺乏研究证明这些铺装在盲人已有的其他线索之外还有增益，暂停了路缘坡道等处的强制铺装要求，直到 2010 年 ADAAG 才用截顶圆点（Detectable Warning）在站台边缘重新标准化；麻省理工的 BATS（Blind Audio Tactile Mapping System）与 Smith-Kettlewell 的 TMAP 则把触觉与声音地图做成可下载、可打印、可自由缩放的产物。“用非文字表达空间信息”这条约束在城市里已经被工程化过一次了：用人手能读懂的凸点代替字；它失败的地方恰恰是人的分辨率——两种纹理太像时，手和眼睛一样读不出来。
如果要做拿三种常见铺装做一组盲测：让人闭眼用手掌分辨刷面混凝土、光面砖与条纹砖，记录混淆矩阵——你会得到一份“人的分辨率”实测表。
参考文献 3
- 10.17226/28910（National Academies of Sciences, Engineering, and Medicine, Tactile Wayfinding in Transportation Settings for Travelers Who Are Blind or Visually Impaired, 2025）
- 旁证：Wikipedia “Tactile paving”（1994 年美国联邦因缺乏研究证据暂停路缘坡道等处的强制铺装要求；2010 ADAAG 规定站台边缘用截顶圆点 Detectable Warning；标准清单含 CEN/TS 15209、AS/NZS 1428.4:2002、DIN 32984:2018）
- 旁证：Perkins School for the Blind 资源页（UNC 的 BATS：Blind Audio Tactile Mapping System；Smith-Kettlewell 的 TMAP：Tactile Map Automated Production，可下载并压印任意街道的触觉地图）
生图提示词
一条铺着凸点的人行道延伸进雾里，路面上滚动着几块颜色不同但纹路几乎一样的地砖，一只手正贴在其中一块上摸索。