Wonderland — 2026-11-07
Wonderland — 2026-11-07
速览（30 秒）
- 组合: 编译器与编程语言设计 × 形式化方法与定理证明 / 手语学与身体语言 × 摄影化学与暗房工艺 / 古文字学与文字起源 × 密码学与信息安全
- 今日火花 Top 3: #1 整座 ZFC 被写成一个符号文件 / #5 摇头是全世界最通用的那一个比特 / #8 占卜记录里自带”事后验辞”
- 可动手候选: #8（给实验记录加一个”验辞”字段）、#6（把连续量压成一个比特加一个位置）、#5（只用点头摇头做问答）
- 值得写长文: #1（把散文删掉之后还剩什么）、#7（不能复制的一次性记录）、#10（介质即密钥）
组合 A：编译器与编程语言设计 × 形式化方法与定理证明 + 如果必须用 LaTeX/数学符号表达所有内容
本期亮点: 这一组是从上一期那张”再写一个 checker”的卡片往下追的第二跳。上一期的落点是”Mizar 没有小可信内核”，这一期撞见的另一条路是 Metamath：整座 ZFC 被写成一个符号文件，验证它只要 500 行 Python。同一个作者（Carneiro）在两条路上各写了一遍——先把 Mizar 的 checker 重写成 Rust，再把 Metamath 的验证器重写进 Lean。而”必须用数学符号表达一切”这条约束，恰好是 Metamath 的原生设计：它从来不需要散文。
💥 #1 — 整座 ZFC 被写成一个符号文件：验证它只需要 500 行 Python
方法论惊讶 9 · 具体 9 · 可行 8
Metamath 的 set.mm 把整座 ZFC 写成一份符号文件——最早的证明标注于 1992 年 9 月，如今主库有超过 26,000 条完整展开的证明，所有数学文本被美元符号包裹，“一个定义无非就是一条公理”；而它的验证器 mmverify.py 只有约 500 行 Python，最大的库”几秒之内就能重新验证”。“必须用数学符号表达一切”在这里不是限制、而是它的原生设计：散文被彻底删掉之后，“一个符号文件”就成了全部知识——而守住这个文件的代码只有一页纸；这条路《数学原理》已经走了一百年。
如果要做挑你们文档里最啰嗦的一段规格说明，改写成一份纯符号声明表（只准出现定义与公理，不准出现解释性散文），写完数一数还剩多少行。
参考文献 1
- Wikipedia “Metamath”（“Raph Levien … implemented a very small proof checker, mmverify.py, at only 500 lines of Python code”；set.mm 的最早证明 dated September 1992）/ 旁证：Metamath Proof Explorer 官方首页（“Inspired by Whitehead and Russell’s monumental Principia Mathematica … over 26,000 completely worked out proofs”）、github.com/metamath/set.mm（README：“Metamath verification is incredibly fast; the largest database available can be re-verified within seconds by some verifiers”）、digama0《Metamath Zero: From Logic, to Proof Assistant, to Verified Compilation》（“All mathematical text is enclosed in $ characters”；“In Metamath, a definition is no more or less than an axiom”）
生图提示词
一整卷摊开的浅色羊皮纸，密密排满抽象的数学符号与几何记号，一个极小的黄铜书签形卡片压在纸卷中央作尺度对比。
💥 #2 — 把一个 Hilbert 系统翻译进 Lean，代价是证明”截断是可采纳的”
方法论惊讶 8 · 具体 9 · 可行 7
Metamath 的 set.mm 走的是 Hilbert 风格（没有截断规则），而 Lean 是自然演绎（截断是核心）；digama0 的 Lean 4 版 Metamath 验证器在深嵌入附录 C 里补上了他当年卡住的那个定理——截断的可采纳性：公理的位置也能换成一条定理来用。“用数学符号表达一切”逼出的第一张真实账单是：换一套符号语法，代价从来不是翻译，而是补上一整套证明义务。
如果要做挑一个你信任的内部格式（配置、DSL、schema），把它翻译成另一种符号语言，然后老老实实算一算：你欠了多少条”可采纳性”证明。
参考文献 1
- github.com/digama0/mm-lean4（“a straightforward verifier for Metamath files written in Lean 4”；作者自述附录 C 完成 “deep embedding of metamath”，并证明了他在 “metamath in metamath” 上卡住的 cut 可采纳性）/ 旁证：arXiv:2403.14064《Lean4Lean: Verifying a Typechecker for Lean, in Lean》（“the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself”）
生图提示词
两套符号系统之间架着一座窄窄的桥，桥面由等距的几何节点串成，桥的另一端立着一块等待被证明的方碑。
💥 #3 — 把证明语言当语言来编译，并且证明这个编译器是对的
装置/原型惊讶 8 · 具体 9 · 可行 7
digama0 的《Metamath Zero: From Logic, to Proof Assistant, to Verified Compilation》把三件事串成一条链：先有逻辑，再有证明助手，最后是一个被验证过的编译器；mm0 把 Metamath 语言编译到一个被形式化的核心语言，再去验证这个编译器本身——按项目自己的说法，Metamath C 这门系统语言的编译器”会吐出一份证明，证明它造出来的程序符合它的规格”。编译器 × 形式化方法的交点在这里是字面的：不是”用编译器写证明”，而是”把证明语言当成一门语言来编译，并且证明这个编译器是对的”。
如果要做把你们内部 DSL 的编译器拎出来，为它写一个小型语义模型，然后只证明一条最关键规则的正确性——先有那一块，剩下的是工程。
参考文献 1
- digama0.github.io/mm0/（“Metamath Zero — a proof language you can check”；“a reader can see exactly what a theorem claims, and a small, independent verifier can confirm its proof”）与 digama0.github.io/mm0/thesis.pdf（“Metamath Zero: From Logic, to Proof Assistant, to Verified Compilation”）/ 旁证：github.com/digama0/mm0（mmc.md 是 Metamath C 的系统语言描述，“whose compiler emits a proof that the program it produced meets its specification”；规格格式”built to be read (it looks rather like Lean)”）、Metamath 官方 Proof Language 文档（us.metamath.org/downloads/ihp2014mm.pdf，“Wffs (well-formed formulas) constructed from variables”，wff 以箭头、否定与全称量词构造）
生图提示词
一台半透明的几何机器，符号块从左侧的料斗进入，在内部被逐层重排成更规整的方阵，右侧吐出一枚发亮的印章形符号。
💥 #4 — 500 行的设计原则能长出四种实现：Python、Common Lisp、Lean 4
同构惊讶 8 · 具体 9 · 可行 7
Metamath 的设计被反复实现：Raph Levien 的 mmverify.py（Python，约 500 行）、Juha Arpiainen 的 Bourbaki（Common Lisp）、Levien 的 Ghilbert，以及 digama0 的 Lean 4 版验证器。上一期的火花是”再写一个 checker”，这一期看到的是更冷的一层：能被反复重写的不是 checker，而是那套让它变小的设计原则。
如果要做把你系统里”小到能被人读完”的那一部分的设计原则写下来（不超过五条），看有没有人愿意用另一种语言实现它。
参考文献 1
- Wikipedia “Metamath”（Ghilbert、Levien 的 mmverify.py、Arpiainen 的 Bourbaki；“Using the design ideas implemented in Metamath”）/ 旁证：github.com/raphlinus/ghilbert（“Ghilbert is a formal proof checker, heavily inspired by Metamath”）、github.com/david-a-wheeler/mmverify.py（“a Metamath verifier written in Python, originally by Raph Levien”）、github.com/digama0/mm-lean4
生图提示词
同一枚抽象符号徽记的四次重绘并排陈列，分别带着不同材质的小底座：一块黄铜、一片黑胶、一枚磨砂玻璃、一块陶瓷。
组合 B：手语学与身体语言 × 摄影化学与暗房工艺 + 如果只能有一个比特的状态
本期亮点: 这一组把两个最”多通道”的领域压到只剩一个比特。手语里最通用、最不可替代的那个比特是摇头（否定）；暗房里最省的那个比特是”显影还是没显影”，而黑白胶片干脆把每个像素都压成一个比特。剩下的全部设计问题只有一个：这一位 0/1 摆在哪儿。
💥 #5 — 摇头是全世界最通用的那一个比特
文化隐喻惊讶 9 · 具体 9 · 可行 8
手语的否定大量依赖非手动标记（摇头），Open Mind 2026 年的《Kinematics of Negative Headshake in Seven Sign Languages》对七种手语的否定摇头做了运动学分析；Veinberg 与 Wilbur 早在 1990 年就指出 ASL 里”是”和”否”各有两个手动手语，而 Pfau 把摇头看作语法化过程的产物。在”只能有一个比特的状态”之下，手语能被保留的最小信息就是”是/否”——而这个比特恰好是全世界手语里最通用、也最难用别的动作替代的那一个。
如果要做把产品里的”是/否”问句单独拎出来，只用最少的信号（一次点头、一次摇头）能不能让对方答对——这是手语用几千年给出的答案。
参考文献 2
- “Kinematics of Negative Headshake in Seven Sign Languages”, Open Mind 10:1636-1677 (2026), DOI 10.1162/opmi.a.394
- 旁证：Veinberg & Wilbur, “A Linguistic Analysis of the Negative Headshake in American Sign Language”, Sign Language Studies 68:217-244 (1990), DOI 10.1353/sls.1990.0013；Pfau, “The grammaticalization of headshakes”, DOI 10.1075/slcs.166.02pfa；arXiv:2409.08162《Cross-Attention Based Influence Model for Manual and Nonmanual Sign Language Analysis》（非手动标记与手语标记共同构成完整意义）；斯图加特大学（“a shake of the head is understood in almost all cultures with very few exceptions”）
生图提示词
一个人的侧脸剪影悬在深青色的虚空里，头顶上方挂着两枚互为镜像的小符号，四周几十条灰白的运动轨迹乱成一团，只有在头部聚成唯一一条锐利的光线。
💥 #6 — 把八比特的灰度塞回一比特：抖动把连续的世界变回黑白
方法论惊讶 8 · 具体 9 · 可行 8
银盐黑白胶片的每个像素只有两种状态，灰度全靠”半色调网点”的空间分布伪造；误差扩散正是把连续调图像量化成 bilevel 图像的做法（“Grayscale digital image halftoning quantizes each pixel to one bit”），Floyd 与 Steinberg 1976 年的算法至今仍是默认答案。“只能有一个比特的状态”在这里不是缺陷，而是暗房的生产条件：你手上只有 0 和 1，唯一的自由度是”把这些 0/1 摆在哪儿”——信息没有减少，减少的只是它待的地方。
如果要做把你最想留住的一段连续量（温度、评分、进度、灰度）压成一个比特加一个位置，然后看看接收端能不能把它重建回来。
参考文献 1
- PMID 18249601《Adaptive threshold modulation for error diffusion halftoning》（“Grayscale digital image halftoning quantizes each pixel to one bit”）/ 旁证：Floyd & Steinberg, “An Adaptive Algorithm for Spatial Grayscale”, Proceedings of the Society of Information Display 17(2), 1976；AM 网点（半色调屏）与 Floyd–Steinberg 两族策略的对比；暗房试纸（test strip）的阶梯曝光实践——一条试纸按 2/4/8/16/32 秒依次曝光，用一次二值判决换回连续量的刻度
生图提示词
一面被切成细密棋盘的深色墙面，黑白两色的方块在网格上起伏成一条柔和的波浪，远处看是渐变，近看只有两种颜色。
💥 #7 — 一张达盖尔版只有一张：手语的表演也是一次性的
文化隐喻惊讶 8 · 具体 8 · 可行 7
达盖尔银版法没有负片，作品因而是”one-of-a-kind”的——但它并不是绝对无法复制：对原版再制一次达盖尔版可以（还顺带纠正了镜像），石印或版画同样能复制，直到 Talbot 1841 年的负片-正片工艺才让照片可以批量复数；而手语作为表演同样是一次性的——ASL 语料库里的每一段视频都是特定手语者在特定时刻的一次演出（ASLLRP 提供前视、侧视与面部特写多机位）。两个”记录不下来”的极端撞在一起：暗房最古老的失败是无法复制，而手语最古老的困境是复制它就等于杀死它——所以手语的”文字化”从一开始就是另起炉灶（SignWriting、Stokoe 记法）。
如果要做给你最想留存的一次”现场”（一次演讲、一次表演、一次对话）做一份负片：先做母版，再想清楚你要复制几份。
参考文献 1
- Wikipedia “Daguerreotype”（“Although daguerreotypes are unique images, they could be copied by re-daguerreotyping the original, a process which also fixes the mirror-image effect. Copies were also produced by lithography or engraving”；无底片、曝光可达一分钟、被摄者必须纹丝不动）/ 旁证：arXiv:2201.07899《ASL Video Corpora & Sign Bank: Resources Available through the American Sign Language Linguistic Research Project》（前视/侧视/面部特写与人工标注）；signwriting.org 存档文献 Valerie Sutton《A Linguistic Comparison: Two Notation Systems for Signed Languages》（比较 Stokoe 记法与 Sutton SignWriting）；Wikipedia “Fingerspelling”（手指拼写在 ASL 日常手语中约占 8.7%、Auslan 约 10%，而在新西兰手语语料中只占 2.5%）；SignWriting 至今只被少数聋人手语者使用（《纽约时报》2002 年：“SignWriting is used today by only a small fraction”）
生图提示词
暗红色的暗房里，一只显影盘托着一张泛着银光的方形底片，旁边摆着一枚同样大小的空托盘，暗示着那张底片无法再生一张。
组合 C：古文字学与文字起源 × 密码学与信息安全 + 如果只能用磁性材料实现，不能有电
本期亮点: 这一组是三条约束里最”物理”的一条：不能有电，于是秘密只能藏在介质参数里——棒子的粗细、磁带走带的速度、刻痕的深浅。另一头是古文字：一条卜辞的格式里，居然自带”事后验辞”这个字段——占卜者当年就为不可复算的占卜留了一个可复算的位置。
💥 #8 — 占卜记录里自带”事后验辞”：最早的实验日志格式
方法论惊讶 9 · 具体 9 · 可行 8
一条完整的卜辞分四段：前辞（占卜时间与贞人）、命辞（问什么）、占辞（结果）、验辞（事后是否应验）；卜辞把”后来验了没有”直接写进记录格式，而兆纹来自背面凿槽加灼烧、解释权在贞人手里（裂痕夹角接近直角读作”是”，远小于直角读作”否”，介于其间为”不确定”）。“只能有一个比特的状态”把这件事推到极致：一次占卜就是一个不可复算的比特，而人类给它配的格式里居然预留了”事后核验”这一栏——甲骨之所以不能”已则弃去之”，恰恰因为得等结果出来核对；今天关于可复现性的全部争论，在记录格式这个层面早就被解决过一次。
如果要做在你们每一次实验记录后面加一个字段：事后核验的结果（应验 / 未应验 / 无法核验）——然后数一数，有多少条记录填得出来。
参考文献 1
- 维基百科”卜辞”（四段结构：前辞/命辞/占辞/验辞；“验辞记录事后占卜事项的结果，评价占卜内容是否被验证”；选材—锯磨—背面凿钻凹槽与圆穴—火烧灼—正面成裂痕—刻写卜辞的流程，以及夹角与吉凶的对应）/ 旁证：甲骨不能”已则弃去之”的原因之一正是要等占卜结果应验；Wikipedia “Oracle bone”（晚商约前 1250–前 1050 年的火卜，用牛胛骨与龟甲，所刻主要是占卜结果记录）、Wikipedia “Oracle bone script”（已知最早的中文书写形态）；arXiv:2607.17849《AlphaOracle》（约 4,500 个甲骨文字中仍有约 3,000 个未释读，因残片与稀疏证据）
生图提示词
一块龟甲占卜骨的特写，骨面刻满抽象古文字形与隐约发光的灼烧裂纹，旁边躺着一根窄骨条，上面刻着一排与主骨呼应的短符号，像一张核验回执。
💥 #9 — 1086 年，沈括记下了指南针系统性偏东：人类第一次记录设备的偏差
文化隐喻惊讶 8 · 具体 9 · 可行 7
《梦溪笔谈》卷廿四《杂志一》：“方家以磁石磨针锋，则能指南。然常微偏东，不全南也”——沈括记下的不只是磁针能指南，还有它总是偏东，即真北与磁北并不重合，而西方要晚一个多世纪才有类似记载；此后《武经总要》前集卷十五又记了指南鱼。原文里他还给出最讲究的一种做法：用新纩中独茧的缕、以芥子许的蜡缀在针腰，无风处悬之，“则针常指南”。在”只能有磁性材料、不能有电”的约束下，这成了唯一一件不靠电的仪器：它不测量，它只是偏——而沈括把这个偏差当成一条事实写进笔记，等于人类第一次把”实现的系统性误差”留在了纸上。
如果要做给你最信任的那个工具写一条”它总是哪里不准”的记录——偏差被写下来，就从玄学变成了可修的量。
参考文献 1
- 维基文库《梦溪笔谈 (四部丛刊本)/卷二十四》原典（“方家以磁石磨针锋则能指南然常微偏东不全南也”；“不缕悬为最善……无风处悬之则针常指南”；成书于 1086 年）/ 旁证：曾公亮、丁度、杨惟德《武经总要》前集卷十五（指南鱼）；《司南酌、盘针及指南鱼新议》（自然科学史方向的期刊论文，讨论磁针指南早于磁石指南与”指南鱼”）
生图提示词
夜里的水碗里浮着一枚鱼形磁针，针尖偏出正北一点点；碗边摊着一册线装古籍，页面上浮着一道细细的斜线标出那点偏差。
💥 #10 — 同一串符号，读法不同就是密文：斯堪塔利的棒径等于磁带的走带速度
同构惊讶 8 · 具体 9 · 可行 7
斯堪塔利是最早的转置密码之一：把羊皮纸缠在棒上写字，接收方要用”同样直径的棒”才能读出来——密钥不是文字，而是那根棒的粗细；同一件事在磁带上是走带速度：改变播放速度会同时改变音高与时长，同一段带按不同速度放就是不同内容。“不能有电、只能用磁性材料”把加密逼到了介质参数上：没有电的时候，秘密藏在纸卷的粗细、磁带的转速和刻痕的深浅里。
如果要做设计一个”介质即密钥”的方案：密钥不写进数据，而藏在读它所依赖的那根棒的粗细、那条带的速度上。
参考文献 1
- Wikipedia “Scytale”（转置密码，接收方需要 “a rod of the same diameter”；经典示例密文 Iotoctydamoaneuynetx，“Every fourth letter will appear on the same line”，还原出来是 “I cannot meet you today”）/ 旁证：磁带播放速度改变音高与时长（FutureLearn “Techniques of tape manipulation”）；一次性磁带密码机 Rockex（1943 年起英加使用；Mk II BID/08/05，1944 年底建于汉斯洛普园）与 Noreen（BID 590，与 Rockex 完全兼容，现藏布莱切利园博物馆）——密钥以六单元字符打孔在密钥带上，每 50 组插一次填充字符；磁带走带速度漂移带来的时基误差亦有专门文献（PMID 7421317）
生图提示词
一条磁性带子在两卷带盘之间绷紧，指针悬在带面上方微微偏向一侧；旁边一根缠着羊皮纸的木棒横放，两者的偏转角度分毫不差。