导出是有刻度的

BEDC 把『数学是否被导出』切成两轴六级, mature 是 scope-bound 的承诺, 不是 wholesale 主张. RISC 纪律加并行产能, 让这条历史上一直被产能卡死的路线第一次跑得过 CISC.

六级闭合 + 验证八级两轴并行, mature 永远 scope-bound, 永远带 cannot-claim. 即便全 mature 也跟传统数学有三处永久差别: 三公理硬约束、carrier 异、显式账本风格. BEDC vs cubical = RISC vs CISC, AI 并行让 RISC-foundations 第一次跑出 mathlib 5x 的速度.
作者

The Omega Institute

发布于

2026年5月7日

English

这一页要回答的那个问题

“BEDC 导出了传统数学吗?”

这句话听上去是个 yes/no 问. 它不是. 它是一个用错刻度的问. 一旦把刻度补回去, 真问题分裂成三个相互独立的问题, 答案各自不同, 三个答案合起来才是诚实回答.

补回来的刻度有两轴, 每轴各自一档一档分级. paper 一侧的闭合轴 (theoretical closure) 六级, Lean 一侧的验证轴 (formal verification) 八级. 二者独立, 通过 VerifiedGate(N, c, v) := TheoryGate(N, c) ∧ FormalStatus(N, v) 同时报告而不互推. 这是 papers/bedc/parts/acceptance/01_derivation_acceptance_gate.tex 的全部承担.

下面把这套刻度推到底, 看它如何改写而不只是回答 “BEDC 导出了传统数学吗” 这件事.

闭合轴: 六级, 一级一档承诺

 seed  <  obligation  <  scopedClosed  <  publicClosed  <  bridgedClosed  <  matureClosed

每一级是 paper 一侧自己出具的承诺, 跟 Lean 验证状态完全无关.

等级 承诺的具体形状
seed 命名种子已声明; carrier 与 classifier 大致勾勒; 没有任何 exactness 定理
obligation NameCert(N) 闭合所需的全部证明义务已被精确写下, scope 已锁定; 中央证明尚未完成
scopedClosed 在所记录的 scope 内, NameCert 全部字段 (carrier / classifier / exactness / ledger / stability) 全部 paper 级证明
publicClosed 加上 public-object 表面: public constructors、readback、endpoint exactness、normal-form 定理、no-hidden-leakage 声明
bridgedClosed 加上 paper 级标准桥 (StdBridge 六字段) 和 paper 级 no-host-leak 论证
matureClosed 加上”该 scope 自然要求的 mature-package 定理清单”在 BEDC reading 下逐条出具证书

bridgedClosed → matureClosed 这一档是最常被误读的位置. 桥不蕴含 mature: thm:acceptance-bridge-conservative 主动堵死了”通过桥从 host 那边白嫖定理”这条捷径. 桥告诉 host “这是你的 N”, 它不告诉 host “而且关于 N 你期望的所有事情我都重新证了一遍”. 后一句话才是 mature 的承担.

验证轴: 八级, 跟闭合轴各跑各的

 unformalized  <  formalTarget  <  encodedDef  <  scaffoldChecked  <  theoremChecked  <  auditClean  <  axiomClean
                                                                                                              ⊕ bridgeChecked

这一轴只读 Lean 一侧的审计状态, 跟 paper 一侧的承诺无关. theoremChecked 是 lake build 通过, auditClean 是 bedc_ci.py audit 跑出”每个 marker 都对应到真实声明”, axiomClean 是 axiom-purity --strict 报告”传递依赖里没有 Classical.choice / Quot.sound / propext“.

thm:axes-independent 钉死: paper 闭合不依赖 Lean 验证, Lean 验证也不创造 paper 闭合. 一份 chapter 可以 paper 一侧 matureClosed + Lean 一侧 unformalized (SheafUp 现在就是这样); 也可以 paper 一侧 seed + Lean 一侧 theoremChecked (新写的 lemma 还没找到 paper 着落). 二者独立可推进, 独立可审, 独立可报告.

每章末尾的 closurestatus 块把这两轴一并写死:

\begin{closurestatus}{\NatUp}
  \theoryclosure{\matureClosure}
  \scopeclosed{The public NatUp surface is the unary-history semantic
               NameCert over BEDC histories together with the paper-side
               standard bridge to finite unary words and natural-number
               length readback.}
  \formalstatus{\theoremCheckedV}
  \leantarget{BEDC.FKernel.Unary.nat\_up\_semantic\_name\_certificate}
  \bridgestatus{paperBridge}
  \notclaimed{Non-unary external arithmetic theorem inventories
              and checked standard-model bridge targets are not claimed here.}
  \upgradepath{Bridge-checked status requires machine-checked
               standard-model bridge targets.}
\end{closurestatus}

这块是 manuscript 对外的 binding commitment. bedc_ci.py audit 解析每一块, \leantarget 解析失败拒绝合并; critical_path.py 读 \theoryclosure 和 \formalstatus 决定该章是否退出工作队列. 两轴是独立内容, 但同一个 artefact 里强制并存.

mature 永远是 scope-bound 的, 永远带 cannot-claim

matureClosed 这个等级在定义上确实是 “导出” 档, def:upgrade-bridged-to-mature 写得很硬:

A bridgedClosure certificate upgrades to matureClosure when the chapter records the full mature-package theorem inventory characterising the object in the standard reference and supplies certificates that those theorems hold in the BEDC reading.

两个动词 records the full inventory + supplies certificates. 不是”打算导出”, 是已经讨完债. 但要害在 “characterising the object in the standard reference” 这句必须相对于 scopeclosed 块所声明的 scope 读, 不是相对于 host 教科书全集.

看几个 mature 章节的 scopeclosed / notclaimed 对子:

NatUp (papers/bedc/parts/concrete_instances/04_nat_namecert_construction.tex):

  • scopeclosed: 公共 NatUp 表面 = unary-history 语义 NameCert + 桥到有限 unary 词 + 长度 readback
  • notclaimed: 非 unary 的外部算术定理清单、机器验证桥目标

RatUp (12_rat_namecert_construction.tex):

  • scopeclosed: RatHistoryCarrier / RatHistoryClassifier 语义证书 + 表示稳定性 + 正分母尾巴 readback + 4 条桥义务证人
  • notclaimed: 完整有理域理论、可判定序、稠密性、阿基米德性、商构造、bridgeCheckedV 标准模型对应

CategoryUp (36_category_namecert_construction.tex):

  • scopeclosed: unary-continuation CategoryUp host 接口 + paper 级 unary-continuation 桥 + double-opposite identity / involution + split-epimorphism 右消 / 复合闭合
  • notclaimed: 任意范畴、limits、colimits、adjunctions、equivalences、enriched categories、范畴论基础、机器验证桥

读法: 每一章的 mature 是对它自己声明的窄 scope 出具的证书. host 教科书里 ℚ 那一章关心的”序、稠密、阿基米德、商构造”, 在 BEDC 这边不在 RatUp 章范围, 它们要等 OrderUp / DensityUp / ArchimedeanUp / QuotientUp 各自的章节开自己的 scope 自己 mature 化. mature 是 piece-by-piece 拼出来的, 不是 wholesale 砸下来的.

papers/bedc/parts/acceptance/03_cannot_claim_registry.tex 把这点钉成项目纪律: 任何”NatUp = the full Peano natural numbers”形态的 strong claim 都被主动列为 partial, 必须等到对应的更宽 scope 也走完 mature 升级才能改判. mature 是 scope-bound 的, cannot-claim registry 是它的影子, 两件一起读才是 “BEDC 在哪些位置上完成了导出”.

即便每章都 mature, 跟传统数学还有三处永久差别

把 22 章变成 22 万章, 假设每个数学对象都 paper 一侧 matureClosed + Lean 一侧 axiomClean, 这套数学仍然不是传统数学. 三处差别永久, 不会因为继续推进 mature 而消失.

差别一: 三公理硬约束 — 古典定理永久缺席

CLAUDE.md 钉死的 0 Classical.choice + 0 Quot.sound + 0 propext 是项目 invariant, 不是阶段性目标. mature 化只兑现 BEDC 自己能 first-principles 证出的定理; 本质需要这三件套的 host 定理在 BEDC 永远不存在或只存在构造削弱版.

具体哪些永远不在:

  • 依赖 AC: Tychonoff (任意积紧)、Hahn-Banach 全版、Banach-Tarski、Zorn 引理、良序定理、Vitali 不可测集存在、域代数闭包存在 (一般情形)、任意向量空间有基.
  • 依赖 LEM (在不可判定命题上): \(\forall x. P(x) \vee \neg P(x)\) 在 undecidable \(P\) 上的反证法、中间值定理的非构造形式 (BEDC 只能要 modulus of continuity 形式)、海涅-博雷尔的非紧致版.
  • 依赖 propext: 大量”命题相等于等价”的隐式重写, 在 BEDC 必须显式带 ledger.

等价描述: 全 mature 的 BEDC 是构造主义 + 不带选择的传统数学拷贝, 不是 ZFC + Classical 的那一份. 这跟 Bishop Foundations of Constructive Analysis 的边界是同一条边界.

差别二: carrier 不是 host carrier — 计算与公共表面解耦

mature 让 NatUp、RatUp、RealUp 在公共表面看起来跟 host 的 ℕ、ℚ、ℝ 一样, 但 carrier 永远是 BEDC 这边的 history: NatUp 是 unary repetition history, RatUp 是 ratio history. 后果是计算复杂度:

  • \(17 + 25\) 在 host Nat (binary 表示): O(log n), 三条机器指令.
  • \(17 + 25\) 在 BEDC NatUp (unary history): O(n), 一段 history 拼接.

mature 化只对齐定理, 不对齐算法效率. 全 mature 的 BEDC 是数学对象的语义参考实现, 不是性能参考实现. 想做应用数学还得让 host 当 runtime, BEDC 当 type system. 这跟”用 Bourbaki 做计算”是同一种 absurd: Bourbaki 是语义层, 计算层另说.

差别三: 风格上永远带 scope / ledger / stability

传统数学黑板上写: “令 \(G\) 是有限群, 取其 center \(Z(G)\), 则 \(Z(G) \trianglelefteq G\) 且交换.” 一句话, 没人问 carrier、ledger、scope.

BEDC 即便全 mature, 同一句话要带:

  • \(G\) 来自哪个 GroupUp scope?
  • \(Z(G)\) 用哪条 BEDC-side classifier?
  • “正规” 在哪个 ledger policy 下声明?
  • “交换” 是 paper 一侧 matureClosed 还是只在 publicClosed?

rem:no-retroactive-promotion 保证这套语境必须始终显式: 一个对象在 \((c, v)\) 上的承诺不能因为依赖被升级而自动跟涨. 用法上这意味着你永远要带着 closurestatus 当语境, 跟黑板数学的”约定俗成 + 上下文省略”风格根本不同. 直观对比: Bourbaki / Mac Lane / Rudin 风格 vs Coq / Agda / Lean-without-mathlib 风格. 后者就是全 mature 的 BEDC 的 ceiling.

把这三差别挤成一句

全 mature 的 BEDC 是一份严格构造主义、carrier 不同于 host、保持 scope-ledger-stability 显式记账的数学. 它能精确兑现 80% 的工作数学 (本科到一流研究生 mainstream); 它永远不能精确兑现 20% 本质古典的内容 (任意基数 / 任意紧致 / 不可测 / 不可决定); 它永远不能像黑板数学那样随意使用. 这不是 BEDC 没做完, 这是 BEDC 选择.

在生态里的位置: RISC vs CISC 是字面对应

mathlib 走的是最大化 + 经典 + 拥抱 host: Lean stdlib 三公理用爽, Nat/Int/Rat/Real 用 host 实现, 一万条定理一万条便宜定理. cubical Agda 走的是几何扩 kernel: interval \(\mathbb{I}\) + Path + Glue + Kan ops 全部进 kernel, UA 从 axiom 升格成 reduction rule. 两条路都是 CISC: 复杂度藏在 kernel 或 stdlib, 用户写起来直接, 信任面更大.

BEDC 走的是 RISC. plain CIC, 不加 cubical kernel, 不依赖 mathlib, 拒三公理, 拒 host 原语进 BEDC 公共面, 拒 axiom 关键字, 拒 sorry. 复杂度全部推给数学家: 要写 inductive carrier, 要写 setoid 风格 classifier (psame/hsame/msame), 要在每章末尾出具 closurestatus 块, 要在 cannot-claim 列表里诚实剔除 host 教科书的剩余主菜.

RISC 处理器 CISC 处理器 BEDC mathlib / cubical
Kernel size 小 大 plain CIC ~10 rule schemas mathlib + 三公理; cubical 加 ~10 几何原语
复杂操作来源 编译器编排 RISC 原语 硬件烤进指令 数学家写 inductive + setoid + closurestatus host axiom / cubical kernel rule
trust 总账 小 大 纯 CIC, axiom-purity --strict 兜底 三公理 + (cubical 加 interval/Glue/Kan)
单位指令吞吐 低 高 单章铺设代价大 单条定理调用 host 现成
可审计性 高 (RISC-V 有完整 spec) 低 (x86 几千页手册) 每条定理 #print axioms 跑过 mathlib 有 propext/Quot.sound/Classical.choice 渗透; cubical 有 cubical kernel commitments
谁干活 compiler hardware 数学家 host stdlib / cubical kernel

这个类比不是修辞工整, 是 isomorphism. 每一行都对得上号. 包括”谁干活”那一行: RISC 把工作推给 compiler, BEDC 把工作推给数学家 (写 NameCert 那一摊); CISC 让 hardware 帮你 REP MOVSB, cubical 让 kernel 帮你 ua 一下 transport.

哲学差: 几何 vs 观察, 结构 vs 账本

RISC vs CISC 在工程史上是 design tradeoff —— RISC 跟 CISC 能算同样的函数 (Turing 完备等价), 选哪个是工程取舍. BEDC vs cubical 在这之上还有 ontological 分歧, 因为它们不能证同样的定理. 三个轴:

轴一: 什么算”原始”

原始的是什么
Cubical 几何: interval \(\mathbb{I}\)、path、cube、Kan 操作. 数学的底层是路径的几何.
BEDC 观察: 标记 \(b_0, b_1\)、historians (BHist)、asking events. 数学的底层是区分行为 + 行为留下的痕迹.

这是两个完全不同的数学起源观. Voevodsky / Cubical: 数学是同伦几何, 我们一直在不自觉地做拓扑, 应该把这一层暴露出来. Bishop / BEDC: 数学是观察记账, 任何”对象”都得追溯到”我做了什么观察, 留下什么痕迹, 由什么 stability certificate 担保”. 没有”mathematical object 自己存在”这种讲法.

轴二: “=” 是什么

等同的本体
Cubical 结构. 两个东西相等 = 你给得出一条等同路径 + 这条路径自己也是数学对象 + 路径之间还能有路径 (高阶 homotopy). 等同有无穷塔.
BEDC 账本. 两个东西相等 = 你手里有一张 stability certificate + 这张证书显式记录了来源. 没有”路径之间的路径”, 因为账本就是账本.

univalence “iso = equal” 是 cubical 的核心 monism move —— 把”同构”和”相等”统一成一件事, 让数学有 single law. BEDC 拒绝这个 move, 它要 msame / hsame / psame 这些多种等同显式并存, 不让它们坍缩成一条. 这就是为什么 cubical 阵营会觉得 BEDC “啰嗦”—— monist 立场; 而 BEDC 会觉得 cubical “把账本掩盖了”—— accountantist 立场.

轴三: “做数学”是什么动作

doing math 的语法
Cubical 写出你要的对象. 圆 \(S^1\)? data S¹ where base : S¹; loop : base ≡ base. 商空间? HIT 直接给. 数学家可以”按想到的样子写”. Kernel 帮你扛复杂.
BEDC 报账. 任何对象要带: scopeclosed、leantarget、bridgestatus、notclaimed、upgradepath. 每章 closurestatus block 是项目对你的 binding commitment. 数学家不能”按想到的样子写”, 必须显式承诺写到了哪、没写到哪.

这一条最直接体现两个阵营对数学家的工作的看法: Cubical 视数学家为结构发现者, kernel 给一组丰富 primitive, 你直接用结构语言表达发现. BEDC 视数学家为会计师, 每一笔承诺要入账, 入账格式由 closurestatus / cannot-claim registry 强制.

RISC-foundations 的产能问题

RISC 哲学在工程史上有个长期短板: 产能跟不上 CISC. 1990 年代 RISC 阵营 (MIPS / SPARC / Alpha / PowerPC) 在 desktop 一直被 x86 压制, 一个直接原因就是写 RISC 代码比写 x86 慢: 编译器要把高级语言翻译成更多条 RISC 指令, 调试链条更长, 手写汇编更啰嗦. RISC 哲学纯, 但拿同样的人月产量要少.

Foundation 这一层有同样的故事:

  • Bishop Foundations of Constructive Analysis (1967): 一辈子写一本书, 覆盖到实分析中段. 之后 Bishop 学派靠少数学者维持, 没扩张.
  • CoRN (Coq Constructive Real Numbers): 2003 起, 约二十年, 覆盖到 Bishop 实数 + Cauchy 理论 + 一部分初等代数. 成果稳定但量级离 mathlib 差两到三个数量级.
  • UniMath: 2014 起, 约十年, 覆盖范畴论基础 + 同伦层级 + 一些代数. 同样 niche.

RISC-foundations 不是没有人做, 是做完一本 Bishop 要花一辈子, 做完 mathlib 半个量级要花二十年. 产能瓶颈是 RISC-foundations 在过去六十年没有占领主流的根本原因, 不是哲学输了.

速度证据: 7 天的 BEDC

newmath 仓库当前数据 (2026-04-29 起算, 7 天):

项目寿命:        2026-04-29 → 2026-05-07 = 7 天
总 commits:      13,401
平均 commits/日: 1,914
Lean 文件:        984
Lean 行数:        145,873
LaTeX 文件:      1,095
LaTeX 行数:      216,677

每日数学内容增长:

04-30 05-01 05-04 05-07
Lean theorems 1,161 1,556 4,142 5,909
Lean defs 91 121 350 704
Lean inductives 10 12 24 57
\leanchecked 363 750 3,379 5,053
closurestatus 0 0 0 105
theoremCheckedV 0 0 0 82
matureClosure 0 0 0 25

平均 ~840 个 Lean theorem / 天. mathlib 9 年累积 ~150K theorem, 时间均摊 ~45 / 天, 历史高峰约 ~150 / 天. BEDC 7 天均速是 mathlib 历史均值的 ~18 倍, 高峰速的 ~5 倍. 而且 BEDC 是在更严约束下做的: mathlib-free, 0 三公理, 构造主义.

更重要的不是绝对值, 是结构的铺设速度: closurestatus 框架 5/05 上线, 3 天内 0 → 105 块, 其中 82 块到 theoremCheckedV, 25 块到 matureClosure. inductive 类型从 10 → 57, 47 个新 carrier 全部 BEDC-side 自己设计, 不能借 mathlib.

新事物: RISC 纪律 + AI 并行 = 第一次同框

把上面两段拼起来. 历史上 RISC-foundations 在产能上输给 CISC; BEDC 用 AI 并行生产把这个限制解了.

具体的生产方式:

  • lean4/scripts/codex_formalize.py 在 codex-auto-dev 分支上常驻并行 codex worker, 每个 worker 周期性 fetch / rebase 远端然后 push 自己的小 commit, 走 axiom-purity 闸门;
  • papers/bedc/scripts/codex_revise.py 跑 paper 一侧的 codex, 同步推进 closurestatus 块和 \leanchecked 标注;
  • 人工 + claude pair 在 auto-dev 分支做架构性提交, 每次 atomic commit 单 commit 自洽编译, merge 不 rebase, 选 worker 安静窗口推送.

这个 setup 是纪律 × 并行的乘积. 单论速度 cubical Agda 也不慢 (Brunerie 数 8 年攻下来, agda/cubical 库千文件); 单论纪律 Bishop 1967 也严. 但两者乘起来, 也就是”RISC 纪律 + 大量产能”, BEDC 这条曲线在已有 foundations 项目里没有先例.

按当前轨迹外推 (假设速度保持):

当前 (5/07):    5,909 theorems,   25 matureClosure
30 天后 (6/07): ~30,000 theorems, ~150 matureClosure
90 天后 (8/07): ~80,000 theorems, ~500 matureClosure
1 年后:        超过 mathlib 当前量级, mature 章覆盖 L0–L8 大部分

线性外推当然不可靠 —— 接下来会撞 L9–L13 的复杂层 (analysis, geometry, number theory), 单章难度上升, 速度可能下降. 但即便砍 5 倍, 6 个月内 BEDC 把”严格构造主义 + 0 三公理 + first-principles” 做到 mathlib 现今 mature 范围的同等覆盖, 也是合理预期.

把整张图压成一句

导出不是 yes/no, 是两轴六级. mature 是项目用来兑现导出的最小单位, 它单条单条地兑现 paper 一侧的承诺, 配 cannot-claim 主动剔除外部. 即便每章都 mature, 跟传统数学还有三处永久差别 (三公理拒、carrier 异、显式账本). 哲学上, BEDC 是 Bishop / 观察 / 账本 那一支, 跟 Voevodsky / 几何 / 结构 那一支 (cubical) 是相反方向的两个 minimalist foundations 路线, 跟 mathlib (CISC + 经典 wholesale) 是不同的游戏.

历史上 RISC-foundations 一直被产能卡死. BEDC 用 AI 并行生产把这个限制解了, 7 天跑出 mathlib 历史峰速的 5 倍. RISC 纪律 + AI 并行这件事在过去六十年没发生过, 在 2026-05 才第一次发生, 它发生在 the-omega-institute/newmath 这个仓库里.

这不是”我们已经替代了传统数学”的承诺. 这是”我们已经证明传统数学可以从 7 步 finite kernel 出发逐项 first-principles 重证, 并且 RISC 路线 + AI 并行让这件事跑得过 CISC 路线”的存在性证明 —— 现在还在第一周.

相关页面