关于 gonzalgo
gonzalgo 分析 Lean 4 和 Metamath 的证明依赖，揭示定理如何依赖未完成证明、公理和受编译器信任的结果。它面向需要可追溯信任评估与依赖分析的形式化证明开发者，并支持 CI 检查和 MCP 调用。
主要功能
- 01追踪继承的未完成证明
- 02查找定理到公理的依赖路径
- 03区分陈述依赖与证明依赖
- 04衡量公理影响范围与变更影响
- 05审计 Lean 4 和 Metamath 库
适用场景
- 01检查 Lean 项目中依赖 sorry 的定理
- 02定位引入公理的证明步骤
- 03评估修改定义的影响范围
- 04在 CI 中运行信任检查
MCP 相关
可选的 MCP 套件提供信任审计、定理到公理的路径、影响分析、公理传播范围、Metamath 审计和库索引工具。
配置
本地服务的配置在各客户端中通用，复制后粘贴到客户端的 MCP 配置文件即可。
工具
本地服务需要在你的电脑上运行后才能读取工具，维护者暂未提供工具列表。
详细介绍
╔════════════════════════════════════════════════════════════════════════════════════════════╗
║ ║
║ ██████╗ ██████╗ ███╗ ██╗███████╗ █████╗ ██╗ ██████╗ ██████╗ ║
║ ██╔════╝ ██╔═══██╗████╗ ██║╚══███╔╝██╔══██╗██║ ██╔════╝ ██╔═══██╗ ║
║ ██║ ███╗██║ ██║██╔██╗ ██║ ███╔╝ ███████║██║ ██║ ███╗██║ ██║ ║
║ ██║ ██║██║ ██║██║╚██╗██║ ███╔╝ ██╔══██║██║ ██║ ██║██║ ██║ ║
║ ╚██████╔╝╚██████╔╝██║ ╚████║███████╗██║ ██║███████╗╚██████╔╝╚██████╔╝ ║
║ ╚═════╝ ╚═════╝ ╚═╝ ╚═══╝╚══════╝╚═╝ ╚═╝╚══════╝ ╚═════╝ ╚═════╝ ║
║ ║
║ where does a formal library spend its axioms? ║
║ ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
#print axioms 会告诉你某个定理是否依赖某条公理。但它无法告诉你公理是在哪一步引入的，而不是继承而来的；也无法告诉你这种依赖会传递多远、有多少依赖本可避免，或者对于某个定理，是哪一步引入了这条公理。这个工具可以做到。
它由同一个程序支持 Lean 4 / Mathlib 和 Metamath 数据库（set.mm、iset.mm、nf.mm），因此可以在相同定义下比较两种基础，而不是仅作类比。
$ pip install gonzalgo
$ gonzalgo index
THE KERNEL INDEX (2026-08-05) what formal libraries rest on
library system theorems unfinished compiler choice
-----------------------------------------------------------------------
Mathlib Lean 4 437,429 0 0 66.62%
Lean core (Init) Lean 4 45,051 0 0 23.91%
Std Lean 4 34,510 0 0 56.66%
Batteries Lean 4 5,249 0 0 32.63%
set.mm Metamath 47,621 0 - 1.22%
...
14 libraries, 603,703 theorems, 0 resting on an unfinished proof.
安装后即可立即运行——无需 Lean、无需构建，也无需文件。以下所有功能都需要 Lean 项目。
纯 Python。支持 macOS、Windows、Linux。唯一的依赖是 numpy。
它能回答的问题
如何知道我的 Lean 证明是否依赖 sorry？
Lean 只会在你输入 sorry 的那一行警告一次。对于几份文件之后使用该引理、因此也尚未证明的定理，它不会发出警告。运行 gonzalgo trust，它会报告所有上游任意位置存在 sorry 的定理，无论相隔多远。
如何找到我从依赖项继承的 sorry？
使用相同的命令。审计会覆盖整个环境，因此你导入的库中的 sorry 会像自己文件中的一样被报告。
我的项目是否在某处使用了 native_decide？
native_decide 的结果通过编译并运行代码、相信其答案得出——受信任的是编译器和运行时，而不是内核；编译器和运行时中也发现过健全性漏洞。gonzalgo trust 会报告它生成的公理 Lean.ofReduceBool 和 Lean.ofReduceNat，以及继承这些公理的定理数量。
这个 Lean 定理实际依赖哪些公理，为什么？
#print axioms 会告诉你是否依赖。gonzalgo why <decl> -a <axiom> 会给出从定理到公理的最短路径，并将每一步标记为陈述依赖或证明依赖——这样你就能看出是哪一步引入了它，以及是否可以改走其他路径。
如果证明依赖尚未完成的内容，我能让 CI 失败吗？
可以。使用 --fail-on-trust，或下方的 GitHub Action。
如果我更改这个定义，哪些内容会受到影响？
gonzalgo impact 会将依赖项分为两类：在陈述中引用该定义的依赖项——其含义会随定义变化；以及仅在证明中使用该定义的依赖项——只需重新构建。
内核 > sorry
它发现了什么
将其用于 Lean 4.32.1 和 Mathlib——790,171 个声明、3,000 万条依赖边——从“整个库”缩小到“可证明可移除”的漏斗如下：
532,605 theorems in Mathlib
─────────────────────────────────────────────────────────────────────
324,808 ██████████████████████████████░░░░░░░░░░ depend on Classical.choice 61.0%
144 ▏ actually SPEND it (entry points)
─────────────────────────────────────────────────────────────────────
69,571 ██████░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░ could be stated without it 13.1%
└─ a ceiling, not an estimate
─────────────────────────────────────────────────────────────────────
805 substitutable sites — a choice-free instance existed, unused
280 declarations whose ONLY route to the axiom runs through one
276 ▏ attributable to a single tactic ────────────────────┐
275 ▏ kernel-verified choice-free after substitution │
4 ▏ kernel REJECTED — and they are exactly the 4 NOT ────┘
▏ attributable to that tactic. The partition was not designed.
这个单独的策略就是 omega。它将六个辅助引理的 Decidable 参数硬编码为 Classical.propDecidable，从不尝试实例合成——因此，像 Nat 上的 a - b = 0 ↔ a ≤ b 这样基础的证明，也会无谓地依赖选择公理。已向上游提交问题；只需修改一个文件即可修复。
让语言模型调用它
$ pip install "gonzalgo[mcp]"
将其添加到 MCP 客户端的配置中：
{
"mcpServers": {
"gonzalgo": { "command": "gonzalgo-mcp" }
}
}
十个工具：audit_trust、why、impact、axiom_reach、metamath_audit、
kernel_index，以及用于从项目生成转储的配套功能。
还有一个 scope 工具，用来说明 gonzalgo 不能做什么——阅读论文、
批改作业、判断文本写得好不好。这样，当模型被问到“这个证明正确吗？”
而输入是一页散文时，它就不会抓起最近的、看起来像证明的工具并返回无意义的结果。
其他每个工具的描述都会重申其前提条件。
它要解决的情况是：生成的 Lean 证明编译失败，很容易发现；但如果它依赖于上游三个引理中的某个 sorry，却仍能编译，就没那么容易发现了，而 Lean 只会在该处的警告中提到一次。
kernel_index 无需文件或网络即可运行，因此模型可以随时调用它，查询已知库的数据。
放进 CI，获取徽章
在任何 Lean 4 项目中添加三行配置。每次提交都会检查定理是否依赖未完成的证明，或是否信任编译器而非内核。
# .github/workflows/kernel-clean.yml
name: kernel-clean
on: [push, pull_request]
jobs:
audit:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: vince-gonzalez/gonzalgo@v1
with:
module: MyProject
然后添加徽章，它直接显示工作流自身的状态——无需额外服务：
徽章实际认证的内容。 不是证明正确——Lean 已经会检查这一点。它认证的是，项目中没有任何定理依赖上游某处的 sorry，也没有任何定理是通过编译并运行代码、而非由内核判定的。
Lean 会警告你刚输入的 sorry，却不会提到三个文件之后悄然继承了它的定理。在 examples/dirty 下的示例中，Lean 报告了 一 条警告，而审计发现了 两 个受污染的定理。
工作原理
your Lean project
│
│ gonzalgo lean-files ./scripts
│ lake env lean scripts/Split.lean
▼
┌───────────────────────┐
│ dependency graph │ one row per declaration:
│ statement │ proof │ KIND · NAME · stmt-deps · proof-deps
└───────────┬───────────┘
│
│ gonzalgo check ← refuses a dump with no proof terms
▼
┌───────────────────────────────────────────────────┐
│ │
▼ ▼ ▼ ▼
amplify eligible why audit
─────── ──────── ─── ─────
where is the how much is which step which sites are
axiom spent, even eligible introduced substitutable, and
and how far for removal? it? which declarations
does it reach? (the ceiling) go clean if you fix
every one
│
▼
lake env lean Rewrite.lean
───────────────────────────
swap the instance in and ask
the KERNEL if the proof holds
内核步骤之上的所有环节都不是凭我一句话就可信的：Substitute.lean 使用
collectAxioms 判定是否可替换，而 Rewrite.lean 会将改写后的证明项提交给
addDecl。我们最初尝试了基于名称的筛查，测得精确率为 41.5%，因此这里完全不读取名称。
快速开始
从你自己的 Lean 项目生成转储，然后针对它提问。
$ gonzalgo lean-files ./scripts # writes the Lean extractors
$ cd my-lean-project
$ lake env lean scripts/Split.lean # -> mathlib_split.tsv
$ gonzalgo check mathlib_split.tsv # verify it actually contains proofs
这个定理为什么需要选择公理？
$ gonzalgo why mathlib_split.tsv Int.mem_box
Int.mem_box
Int.mem_box
--proof--> Int.mem_box._proof_1_5
--proof--> Classical.propDecidable
--proof--> Classical.choice
每条边都会标记为 stmt 或 proof，这正是关键：证明边通常可以通过修改策略来绕开，而语句边则不能在不改变定理含义的情况下触碰。只有全由证明边构成的路径，才意味着值得修补某个声明。
如果我修改这个，会有什么内容出问题？
$ gonzalgo impact mathlib_split.tsv Nat.decLe
Nat.decLe
reached transitively 398,968 (295,411 of them theorems)
── direct ──
in a STATEMENT 626 API surface: changing the
type changes their meaning
in a PROOF only 4,225 insulated: a type-preserving
change costs a recompile
反向运行 why。语句/证明的区分正是其价值所在：某个声明的类型若提到了目标，就说明目标属于它的 API，因此目标变动时，该声明的含义也会随之改变，其使用者可能需要重写。若它只是在证明中调用目标，则只需重新构建。简单地列出“谁在使用它”无法区分两者，因此也无法判断修改是否安全。
某个公理的影响有多广，又在哪里被用到？
$ gonzalgo amplify mathlib_split.tsv
axiom Classical.choice
theorems 532,605
dependents 324,808 reach 61.0%
entry points 144 2.704e-04 per theorem
amplification 2,256x
其中有多少部分原则上可以移除？
$ gonzalgo eligible mathlib_split.tsv
statement CHOICE-FREE, proof dep 69,571 13.1% <- eligible
...
ceiling on removable classical dependence: 13.1%
如果某个定理的陈述提到了依赖选择公理的内容，无论如何证明，都不可能让它摆脱对选择公理的依赖。只有其余定理才是候选，而这个数值只是上限，并非估算。
Metamath，相同的测量指标：
$ gonzalgo mm set.mm iset.mm nf.mm
set.mm
theorems 47,621
logical axioms (|-) 1,561 used 1447
median entries per axiom 2.0
overall amplification 292.1x
内核信任配置
gonzalgo profile 会将一个库所依赖的基础写入 JSON，供提交到版本库并由其他程序读取：
$ lake exe gonzalgo MyProject myproject.tsv
$ gonzalgo profile myproject.tsv --name MyProject -o kernel-trust.json
{
"ktp_version": "0.1",
"subject": { "name": "Lean core + Std", "revision": "…", "system": "Lean 4" },
"counts": { "theorems": 88842 },
"unfinished": { "theorems_reaching": 0, "axioms": ["sorryAx"] },
"compiler_trusted": { "theorems_reaching": 0 },
"assumptions": [
{ "name": "Classical.choice", "kind": "optional",
"entry_points": 24, "reach": { "theorems": 31516, "fraction": 0.3548 },
"via": "both" }
]
}
两条规则起到了大部分作用。未测量的字段为 null，绝不是 0——Metamath 没有 native_decide，因此它的 compiler_trusted 计数为不适用，而不是零；写成零就等于声称了没人提出过的结论。并且，工作区有未提交更改时会拒绝填写 revision，因为如果提交记录无法说明测量内容，其他人就无法复现这份配置。
我们刻意不提供汇总分数。定理要么能到达未完成的证明，要么不能；拿它和其他任何指标求平均，都会凭空制造测量本身并不具备的精确度。
完整规范：Kernel Trust Profile 0.1（Zenodo）。
示例见 examples/lean-core-kernel-trust.json。
覆盖范围与放大倍数
在内联和因式分解操作下——这类操作会改变库的写法，而非其证明内容——依赖项集合保持不变，而入口点集合则不然。将每个公理的所有用法都改为经由一个网关引理，或将该引理内联，都能在不改变任何定理的情况下，让放大倍数在 1 到依赖项数量之间任意变化。
因此，覆盖范围适合在库之间比较；放大倍数描述的是单个库的因式分解方式。 工具会同时报告两者，本 README 也明确说明了它们的区别，因为这种区别很容易被忽略，而一旦忽略，代价很高。
值得了解的一项风险
在 Lean 4.32 中，除非调用时使用 value? (allowOpaque := true)，否则 ConstantInfo.value? 对定理会返回 none；而且这一行为在不同版本间有所变化。按直觉编写的提取器会记录不到任何证明项：每个定理的值都会返回空，分析过程悄悄测量的是命题，并将其报告为证明。输出看起来毫无问题——只是库显得比实际更干净。
gonzalgo check 就是为此而设，每个子命令都会先运行它，再信任转储内容：
$ gonzalgo check bad_dump.tsv
ERROR: bad_dump.tsv: 532,605 theorems, none carrying a proof term.
The extractor called `ConstantInfo.value?` without `(allowOpaque := true)` ...
它会直接报错，而不是发出警告。没有证明项的转储不会只产生稍差的数字，而是会产生看似可信、实则错误的数字。
库的使用
from pathlib import Path
from gonzalgo import lean
dump = Path("mathlib_split.tsv")
lean.check_dump(dump)
g = lean.load(dump)
g.path_to("Int.mem_box", lean.AXIOM) # why
g.entry_points(lean.AXIOM, among="T") # where it is spent
g.dependents(lean.AXIOM) # boolean mask over all nodes
lean.eligibility(dump, g).ceiling # what fraction could be removed
作为 Lake 包使用
此仓库本身也是一个 Lean 库，因此可以将提取器作为依赖项，而不必复制并修改文件。在你的 lakefile.toml 中添加：
[[require]]
name = "gonzalgo"
git = "https://github.com/vince-gonzalez/gonzalgo"
这样完全不需要临时文件——它会在运行时导入目标模块：
$ lake exe gonzalgo MyProject myproject.tsv
importing MyProject ...
declarations written: 204543
now run: gonzalgo check myproject.tsv
模块导入的所有内容都会包含在内；第五列输出会记录每个声明来自哪个模块，以便之后将你的项目与其依赖项区分开来。
如果你更愿意在文件内部调用它，这个库只需两行：
import Gonzalgo
#eval Gonzalgo.dumpSplit "myproject.tsv"
该库只依赖 Lean——我们刻意不依赖 Mathlib，因为在这里固定 Mathlib 版本会迫使每个被测项目都采用该版本。
仅针对 Lean core 和 Std 运行，结果如下：
axiom declared direct theorems
sorryAx yes 0 0
Lean.ofReduceBool yes 0 0
Classical.choice yes 32 31,516
propext yes 13,246 70,150
CLEAN: no theorem here rests on an unfinished proof or on the compiler.
88,842 个定理中，有 32 个声明使用了 Classical.choice，而 31,516 个声明继承了它。
已提供的 Lean 源文件
gonzalgo lean-files 会将这些文件写入你选择的目录。对于 Split.lean 的用途，优先使用上面的 Lake 包；这些文件用于超出提取范围的分析，以及未使用 Lake 的项目。
| 文件 | 功能 |
|---|---|
Split.lean | 声明图，将语句依赖项和证明依赖项分列显示 |
Substitute.lean | 重新合成每个经典可判定性位置，并通过 collectAxioms 分类 |
Rewrite.lean | 重写证明项，并由内核检查替换结果 |
OmegaFix.lean | 修补版 omega 前端——仅作演示，见下文 |
Extract.lean | 较早的图转储工具，已由 Split.lean 取代 |
Substitute.lean 使用内核自身的记账机制判断是否可替换，而不是依据名称。基于名称的筛选在 set.mm 上测得的精确率为 41.5%；其典型失效情况是某个引理将选择公理移入前提，而不是将其消除。这看似有所进展，实则不然。
背景
本包是论文 Where Formal Libraries Spend Their Axioms:
A Cross-Foundation Measurement, and an Avoidable Classical Dependency in Lean's
omega 背后的工具——10.5281/zenodo.21769846。
将其应用于 Lean 4.32.1 和 Mathlib（790,171 个声明、30M 条依赖边）后，发现有 280 个声明，其通向 Classical.choice 的唯一途径经过可替换位置；其中 276 个可归因于 omega 判定过程中的单一原因。重写全部 280 个证明项并提交给内核检查：276 个通过，4 个未通过，275 个不再依赖 Classical.choice。
引用来源
- keithadler/tenet — 一个独立的 Lean 4 内核检查器，使用 C#/.NET 编写。它的
tenet why会追踪是哪一步引入了公理，这与 gonzalgo 的 Lean 版why要回答的问题相同。
作者与引用方式
Vince Gonzalez — ORCID 0009-0005-3640-014X · f-keys.com/gonzalgo
@software{gonzalgo,
author = {Gonzalez, Vince},
title = {gonzalgo: axiom provenance for Lean 4 and Metamath},
year = {2026},
url = {https://github.com/vince-gonzalez/gonzalgo},
doi = {10.5281/zenodo.21769846},
license = {Apache-2.0}
}
已存档于 Software Heritage，标识符为
swh:1:dir:871f62fca5b737da9b4f99516d3689d23ffbc60d；无论此仓库是否解析成功，它都能确定对应存档。包含来源、访问记录和锚点的限定形式，见 codemeta.json。
论文。 两篇论文均采用 CC-BY 许可，且均附带存档，可通过一条命令从随附数据重新生成所有图表。
- Where Formal Libraries Spend Their Axioms — 10.5281/zenodo.21769846
- Why Tactic-Level Rates Cannot Attribute Classical Dependencies in Lean — 10.5281/zenodo.21853489
许可证
Apache-2.0。详见 LICENSE 和 NOTICE。
OmegaFix.lean 是 Lean 4
src/Lean/Elab/Tactic/Omega/Frontend.lean 的修改副本，版权所有 (c) 2023 Lean FRO, LLC，依据 Apache-2.0 许可使用。文件顶部的声明列出了对它所做的修改。此文件旨在演示所提议的修复能够编译并生成不依赖选择公理的证明；它不能替代 omega，也不应被用作替代品。
与 Lean FRO 或 Mathlib 社区无关联，也未获其认可。
╔════════════════════════════════════════════════════════════╗
║ ║
║ ███████╗ ██╗ ██╗███████╗██╗ ██╗███████╗ ║
║ ██╔════╝ ██║ ██╔╝██╔════╝╚██╗ ██╔╝██╔════╝ ║
║ █████╗ █████╗█████╔╝ █████╗ ╚████╔╝ ███████╗ ║
║ ██╔══╝ ╚════╝██╔═██╗ ██╔══╝ ╚██╔╝ ╚════██║ ║
║ ██║ ██║ ██╗███████╗ ██║ ███████║ ║
║ ╚═╝ ╚═╝ ╚═╝╚══════╝ ╚═╝ ╚══════╝ ║
║ ║
║ · C R E A T I V E · ║
║ ║
║ ──────────────────────────────────────── ║
║ ║
║ Vincent Gonzalez ║
║ f-keys.com ║
║ ORCID 0009-0005-3640-014X ║
║ ║
╚════════════════════════════════════════════════════════════╝
评论
一个开放协议，规定了 AI 应用如何以统一方式连接外部工具与数据源。客户端负责与模型对话，MCP 服务负责提供工具、资源和提示模板，两者通过标准消息通信，同一个服务可以被不同客户端复用。