Wonderland — 2026-11-05

Wonderland — 2026-11-05

速览（30 秒）
  • 组合: 编译器与编程语言设计 × 形式化方法与定理证明 / 生态学与复杂系统 × 仪式与表演人类学 / 折纸与多面体折叠 × 叙事学与文学结构
  • 今日火花 Top 3: #1 第二个 checker 是 1995 年就有人想过的事 / #5 同步是一种多人游戏机制 / #8 1991 年就有人把故事折进纸里
  • 可动手候选: #8（做一本 Storigami）、#1（给校验器找一个异构替身）、#5（做一次同步实验）
  • 值得写长文: #2（四色定理的信任边界走了九年）、#7（没有管理员的蚁丘）、#10（同一张纸，两种读法）

组合 A：编译器与编程语言设计 × 形式化方法与定理证明 + 如果时间倒回 1995 年，用当时的技术怎么实现？

本期亮点: 这一组从上一期那张”再写一个检查器”的卡片往下追了一步，追到了一个更古老的现场：Mizar 的 checker 是 1977 年 8 月在 CDC 6000 上用 Pascal 写成的，2023 年有人用 Rust 把它整个重写了一遍，8 核 11.8 分钟验完整个数学库，顺手抓出 4 个健全性 bug 和 1 个正被 46 篇文章依赖的 bug。于是”1995 年”这条约束落到了实处：当年你手上只有一份 Pascal 源码，而”再写一遍”要同时读懂并重写一个跑了二十年的证明内核；今天这件事的成本降到了一个周末。

💥 #1 — 第二个 checker 是 1995 年就有人想过的事：只是那时没人写第二个 Mizar

方法论惊讶 9 · 具体 9 · 可行 8

Mizar 的 checker（MIZAR-QC）于 1977 年 8 月在 CDC 6000 上用 Pascal 写成；2023 年的 mizar-rs 用 Rust 整体重写了 checker 与 analyzer，是全世界第一个、也是唯一一个外部实现，8 核 11.8 分钟验证整个 MML，比原 Pascal 实现快 4.8 倍。在 1995 年这条约束下，这个动作的唯一门槛就是”再写一遍”：那时你手上只有一份 Pascal 源码，写第二个 checker 意味着同时读懂并重写一个已经运行了二十年的证明内核，成本高到没人做；今天一个周末就能换一门语言重写它——审计的门槛从”读代码”降到了”再写一遍”。

如果要做给你们项目里最信任的那个校验器写第二份实现——换一门语言、换一种算法，然后造一个让两者结论不同的输入；把它当成你团队的第一个异构替身。

参考文献 2
  1. arXiv:2304.08391《Reimplementing Mizar in Rust》(Carneiro 等，ITP 2023，LIPIcs v268；“the first and only external implementation of these components”、“verify the entire MML in 11.8 minutes on 8 cores, a 4.8x speedup over the original Pascal implementation”)
  2. 旁证：MatRud2005《Mechanized Mathematics and Its Applications》Vol.4 No.1（“In late August 1977, the implementation of MIZAR-QC was completed in Pascal on a CDC 6000”）；Mizar 官方史（1989 年 1 月 1 日 MML 正式开库，2005 年库里已有 855 篇文章）；论文自陈的难处——“Mizar does not have a ‘small trusted kernel’“，所以”checking Mizar proofs entails following Mizar closely”，当年没人做第二个 checker 并不只是懒；Lean Kernel Arena（arena.lean-lang.org：多个独立 checker 跑同一套用例——该拒绝的无效证明、该接受的有效证明、无预期结果的边界情形各成一列，先按”错误接受”数量排序，崩溃与超时也算弃答）
生图提示词

暗色工作台上并排放着两台全手工的仪器：左边是黄铜齿轮与玻璃透镜，右边是挂着配重的小柱；两台都对着中央一个发光的半透明小方块，方块前的桌面上摊着一张空白的纸和一支削好的铅笔。

img-2026-11-05-1.png

💥 #2 — 四色定理在 1995 年还只是”手写证明 + C 程序核对有限情形”

文化隐喻惊讶 8 · 具体 9 · 可行 6

1995 年 Robertson、Sanders、Seymour、Thomas 发布的四色定理新证明沿用 Appel–Haken（1976）的论证思路，但用 C 程序核对巨型案例与大型案例；把整件事整机化要等到 2004 年——Gonthier 的《A computer-checked proof of the Four Colour Theorem》第一次由 Coq v7.3.1 完整检查通过。1995 年的信任边界画在”C 程序”上：机器只负责有限枚举，不负责推理；这条线花了九年才从”程序”挪到”证明”——而 1995 年的 Coq 距离 1989 年那个被称为”成熟系统”的 V4.10 才六年，把整座数学的信任边界搬进一台机器，在那台机器上还是一个奢侈的决定。

如果要做翻一下你们项目里最关键的自动化：它检查的是”结论”还是”推理”？把这两件事分开写进 README 的一行——你会看见自己的信任边界画在哪。

参考文献 2
  1. Gonthier《A computer-checked proof of the Four Colour Theorem》(2004，Coq v7.3.1；文中回顾 1995 年 RSST 版用 C 程序检查大案例与巨型案例)
  2. 旁证：Rocq（Coq）官方历史（CoC 出现在 1985 年；V4.10 于 1989 年 5 月 1 日发布，官方文档称其”was then a mature system”，跑在 CAML V2.6 上）
生图提示词

一条水平时间轴上并排三样东西：左边一台 1976 年的工作站，中间一叠标着 C 的纸卡，右边一台安静发光的证明机器；一条红色虚线标着”信任边界”，正从纸卡一寸寸挪向机器。

💥 #3 — 一个 bug 传染了 46 篇文章：证明的依赖图就是一条供应链

同构惊讶 8 · 具体 9 · 可行 7

mizar-rs 报告在原实现里找出 4 个健全性 bug（尚未被 MML 利用），以及 1 个非关键 bug——后者正被 MML 中 46 篇文章真实依赖。1995 年的 MML 是一摞印在《Formalized Mathematics》纸上的相互依赖：修一条被反复引用的引理，等于让几十篇论文同时失去地基，而那时没有 CI、没有影子构建机，唯一的保险是把整库重验一遍——今天这要 11.8 分钟（8 核），当年则是一台 CDC 6000 上的整库重跑。

如果要做给你项目最底层那个”谁都在用”的模块画一张传染图：谁依赖它、它依赖谁；然后挑一个从没有人端到端重跑过的下游，做一次复验。

参考文献 1
  1. arXiv:2304.08391摘要（“four soundness bugs in the original (which were not being exploited in MML), in addition to one non-critical bug which was being exploited in 46 different MML articles”）/ 旁证：Mizar 的《Formalized Mathematics》期刊（1989 年起按卷期出版，2005 年 855 篇）
生图提示词

一叠纸牌层层叠放，纸牌之间用细线相连；其中一张纸牌的角上破了一个小孔，红色沿着连线蔓延到四十六张纸牌的边缘。

组合 B：生态学与复杂系统 × 仪式与表演人类学 + 如果必须用游戏机制来表达

本期亮点: 把这两个领域强行放进游戏机制里，意外地撞出了三个现成的坐标：生态学与政治学共享一个词——“生态”（Long 1958 的”游戏生态”）；人类学用实验证明仪式的黏合剂其实是同步；蚁巢则是一台没有管理员、只用痕迹通信的机器。三张卡分别落在”系统”、“节奏”和”日志”上。

💥 #4 — 社区不是一台机器，是同时开着的一堆局：Long 1958 的”游戏生态”

同构惊讶 8 · 具体 9 · 可行 6

Norton E. Long 1958 年在《The Local Community as an Ecology of Games》（American Journal of Sociology 64: 251–261）里把地方社区描述成一个”游戏的生态”：同一批人在不同机构里同时开不同的局，谁也无法置身事外；Lubell 2013 年在《Governing Institutional Complexity: The Ecology of Games Framework》（Policy Studies Journal, 10.1111/psj.12028）里把它改造成分析框架，并画出一张”游戏生态”的二元网络图。“生态”这个词在生态学与政治学里其实是同一个：系统不是一台机器，而是很多局并发运行的集合；规则不是机制，而是生态位。

如果要做画出你们团队同时在玩的”局”（发版评审、需求排期、事故复盘、招人），标出每局争夺的资源——你会发现大部分冲突不是某局内部的问题，而是两局之间生态位的重叠。

参考文献 1
  1. Lubell (2013)《Governing Institutional Complexity: The Ecology of Games Framework》Policy Studies Journal, 10.1111/psj.12028（“our adaptation of Norton Long’s concept of the ‘ecology of games’“，含 agent-based model 与二元网络图）/ 旁证：Long (1958) AJS 64:251–261
生图提示词

一张俯视的桌游盘被切成一格一格的池塘，每格池塘里抽象的生物正在争夺光斑，棋盘边缘散落着几张写着不同规则的卡片。

💥 #5 — 同步是一种多人游戏机制：三个实验证明同步行动的人合作更多

方法论惊讶 9 · 具体 9 · 可行 7

Wiltermuth 与 Heath 2009 年《Synchrony and cooperation》的三个实验发现：同步行动的人合作更多；Whitehouse 等人比较九种仪式的田野实验发现，带同步身体动作的仪式更可能提升利他态度，其机制是”与他者的合一感”（Human Nature 24: 115–125）。把同步做成游戏机制，它就从一个文化现象变成一个可调参数：共享节拍、齐步走、一起数三秒——仪式之所以黏合群体，可能只是因为它把每个人的时钟对齐了一格。

如果要做在下一次团队会议里做一次同步实验：所有人同时写下三个关键词，再各自独立写一遍，比较两种条件下的产出重合度——你会得到一个可调的”同步旋钮”。

参考文献 2
  1. Wiltermuth & Heath《Synchrony and Cooperation》Psychological Science 20(1): 1–5, DOI 10.1111/j.1467-9280.2008.02253.x（三个实验）
  2. 旁证：Whitehouse et al.《How do rituals affect cooperation? An experimental field study comparing nine ritual types》Human Nature 24: 115–125, DOI 10.1007/s12110-013-9167-y（九种仪式，带同步身体动作者更利他，机制为合一感）；《Let’s dance together: synchrony, shared intentionality and cooperation》(PMC3737148)
生图提示词

一圈没有五官的人影围成一圈，胸口各亮着一颗同频闪烁的光点；圈中央一台巨大的机械节拍器，影子随节拍一齐起伏。

img-2026-11-05-2.png

💥 #6 — 游戏与仪式的分界线不是形式，是相信

文化隐喻惊讶 8 · 具体 9 · 可行 6

Huizinga《Homo Ludens》（1938）提出”魔法圆”：圆内”绝对而特殊的秩序”统治一切；但他在借 Granet 描述中国宗族时又指出，游戏与仪式的真正差别在信仰——游戏是自愿的、其规则可疑的，仪式是强制的、其规则被相信的。这条分界线一旦做成游戏机制，就会得到一个罕见的中间态：给玩家一套必须遵守的规则，同时明确告诉他”你不需要相信这些规则”——这就是仪式性游戏：假装严肃地玩。

如果要做挑一个团队里”仪式性”的动作（周会、复盘、站会），问一句：去掉”大家相信这有用”这一层，它还剩下什么？剩下的那部分，才是它真正的机制。

参考文献 6
  1. Huizinga《Homo Ludens: A Study of the Play-Element in Culture》(1938；魔法圆：“Inside the play-ground an absolute and peculiar order reigns”)
  2. 旁证：arXiv:2601.12872《Who Moves the Deity? Mechanics, Participation, and Attributed Agency in Himalayan Rath Carrying》（用运动控制与合成力学拆解抬神轿的仪式，分出”知道目的地
  3. 准备载荷变化
  4. 影响局部移动
  5. 赋予事件意义”四层参与，神谕提议把”神的主动”接到”人的责任”上）；PMID 28656521《Strategic interactions: Games of the Ju
  6. ‘hoan》（棋盘、纸牌、手势三种策略游戏，主要由成人玩，动摇了”游戏必有深层意义”的说辞）
生图提示词

荒地上一个发光的圆环把几个人圈在里面，他们按同一个姿势共舞；环外一个拿放大镜的旁观者正透过圆环往里看。

💥 #7 — 一座没有管理员的蚁丘：环境的痕迹就是游戏里的消息

装置/原型惊讶 8 · 具体 9 · 可行 7

Grassé 1959 年用 stigmergy（经由环境进行的间接协调）描述白蚁建巢，此后它成为群智能的核心概念之一；Galatolo 等人 2018 年甚至把”stigmergic memory”做成与 LSTM 同级的记忆机制。把 stigmergy 搬进游戏设计，就得到一种罕见的多人结构：玩家之间不说话、不协商，他们只修改环境；环境就是日志，下一步由痕迹决定——像蚁丘，也像服务器上一堆彼此不知情的缓存。

如果要做做一个只有”痕迹”没有”聊天”的小游戏：玩家只能留下记号，下一位玩家只依据记号行动——你会立刻尝到 stigmergy 的乐趣与误解。

参考文献 2
  1. Grassé (1959)《La reconstruction du nid et les coordinations interindividuelles chez Bellicositermes natalensis et Cubitermes sp. la théorie de la stigmergie》Insectes Sociaux
  2. 旁证：Wikipedia “Stigmergy”（1959 年提出，经环境间接协调，群智能核心概念）；Galatolo, Cimino & Vaglini (2018)《Using Stigmergy to Incorporate the Time into Artificial Neural Networks》
生图提示词

一座泥土蚁丘的剖面，切面上是密密麻麻的通道；一只只半透明的小虫在通道里各自留下发亮的痕迹，痕迹连成一张发光的网。

组合 C：折纸与多面体折叠 × 叙事学与文学结构 + 如果必须把它做成一个实体装置

本期亮点: “必须做成实体装置”这条约束把叙事学逼回了纸：1991 年就有人把故事折进纸里（Storigami），2015 年有人做了折纸互动书，把”折一下”变成”解锁下一段”。更硬的一条来自折纸自己——平面折叠是图灵完全的，所以”这个故事能不能被折出来”居然是个有复杂度的问题。

💥 #8 — 1991 年就有人把故事折进纸里：讲完，纸上留下一个三维惊喜

装置/原型惊讶 9 · 具体 9 · 可行 9

Christine Petrell Kallevig 在 1991 年写出第一本 Storigami（storytelling + origami）：一边读故事，一边把纸折成动作、场景或角色的形状，等故事结束，纸里留下一个意外的三维图形；2015 年 Julie Stephen Chheng 把这条路线推到互动书的尺度——读者折起、展开书的不同部分，从而解锁叙事的不同面向。在”必须是实体装置”的约束下，叙事的载体不再是按钮而是折痕：一次折叠就是一次选择，一次展开就是一次回溯；而且这套装置不需要电——纸自己记得它被折过。

如果要做拿一篇你写的文章做一本 Storigami：读到每个动作就折一次，读完把纸完全展开——你会立刻看见这篇文章的骨架是不是一条真的故事线。

参考文献 2
  1. Kallevig《Fold-Along Stories: Quick & Easy Origami Tales For Beginners》(ISBN 0962876992；1991 年首本 Storigami)
  2. 旁证：Storigami 作者页（“Each fold illustrates an action or character from the story, so by the time the story is over, a surprise origami figure is magically created”）；Fast Company《An Interactive Story Unfolds In This Amazing Origami Book》(2015, Julie Stephen Chheng：“Users fold and unfold different sections of the book, and by doing so, unlock new aspects of the narrative”；同一道折痕朝一个方向折出平静的海滩，朝另一个方向折出海怪的触手；她的前作《Poemes en Pieces》已让读者用剪片拼装故事)
生图提示词

一双手捧着一册摊开的书，一株纸做的树从书页的折缝里长出来，纸的层叠一圈圈像年轮，桌面是温润的木色。

img-2026-11-05-3.png

💥 #9 — “这个故事能不能被折出来”是个计算问题：平面折叠是图灵完全的

方法论惊讶 8 · 具体 9 · 可行 6

1996 年 Bern 与 Hayes 证明平面图折纸的全局可折性是 NP 难的，这条结论沉睡了二十年，直到 Akitaya 等人 2016 年修补并加强了证明，2025 年 2 月的修订版《Flat origami is Turing complete》把结论推到最强：平面折叠能模拟图灵机。把叙事的分支折进一张纸，就等于要求这张纸可折——而这是一个图灵完全的判定问题：不是每个分支故事都真的能被折出来，有些折法在数学上根本不存在。叙事学里”这故事还能不能讲下去”，第一次有了计算复杂度。

如果要做拿你最想讲的一个故事，试着只用一次折叠讲完它（不许翻页、不许跳读）——你会体验到”可折性”有多受限。

参考文献 2
  1. arXiv:2309.07932《Flat origami is Turing complete》(Akitaya, Cheung, Demaine, Horiyama, Hull, Ku, Tachi, Uehara；v4 2025-02-26，文中回顾 Bern & Hayes 1996 与 [ACD+16] 2016 的修补)
  2. 旁证：arXiv:2506.12659（全局可折性 NP 难，Bern & Hayes；折痕图的重叠图建模）；arXiv:2211.13219《Automating Rigid Origami Design》（把刚性折纸设计表述为离散优化问题，直接称作 “the rigid origami game”——折纸这一行连设计本身都用游戏来命名）
生图提示词

一张白纸悬在深色空间中央，纸面上密布发光的折痕线，线条逐渐长成一张网；网的一角亮起一个小小的停机符号。

💥 #10 — 折纸算命：同一张纸，两种读法（随机裁决 vs 神意）

文化隐喻惊讶 8 · 具体 9 · 可行 6

日本神社与寺院的御神籤（omikuji）是印在纸签上的随机短诗；“kuji”这个词本身就有双重含义：既指”用随机机会给出不偏不倚的裁决”，也指”在神意适合介入之处请示神的判断”；这套做法被认为源自中国的求签（kau chim，竹筒签）。叙事学的”歧义”在东亚有一张现成的纸：一张折过的纸签既是随机抽取的结果，也是神的回答——同一张纸，两种读法，差别只在于你承认哪种解释权。

如果要做给你的文章写一段”签文”：同一个故事给两种读法（读者以为的 / 你真正的），不给结论——你会体验到解释权握在谁手里有多重。

参考文献 3
  1. Wikipedia “O-mikuji”（御神籤：神社寺院里的随机纸签；kuji 的双重含义——随机机会的不偏不倚
  2. 神意判断；源自中国 kau chim 的竹签）
  3. 旁证：纸签与折纸作为占卜载体（神社授签的传统形态）
生图提示词

神社签筒里抽出的一枚纸签，纸签一半浸在金色的水里、一半露在光里；纸上的字从左往右读是一种意思，从右往左读是另一种。