gonzalgo について
gonzalgoは、Lean 4とMetamathの形式証明ライブラリを監査するツールで、証明依存関係を調べる研究者やメンテナー向けです。未完成の証明やコンパイラーへの信頼が伝播する範囲を追跡し、定理の命題と証明の依存を区別します。
主な機能
- 01上流の`sorry`とコンパイラー信頼の追跡
- 02定理から公理への依存経路の表示
- 03命題依存と証明依存の分離
- 04変更影響と公理の到達範囲の分析
- 05Lean 4およびMetamathライブラリの監査
- 06カーネルトラストプロファイルの生成
活用シーン
- 01未完成の証明に間接依存する定理の特定
- 02公理依存を導入した具体的な手順の特定
- 03定義変更による下流定理への影響の評価
- 04CIでの証明トラスト状態の確認
MCP 対応
`gonzalgo[mcp]`をインストールすると、`gonzalgo-mcp`を介してMCPクライアントに信頼性監査、依存経路、影響分析、公理の到達範囲、ライブラリ索引などのツールを公開します。
設定
ローカルサーバーの設定はどのクライアントでも共通です。コピーしてクライアントの MCP 設定ファイルに貼り付けてください。
ツール
10掲載時のツール一覧 · 2 週間前に更新
このツールにパラメーターはありません。
詳細
╔════════════════════════════════════════════════════════════════════════════════════════════╗
║ ║
║ ██████╗ ██████╗ ███╗ ██╗███████╗ █████╗ ██╗ ██████╗ ██████╗ ║
║ ██╔════╝ ██╔═══██╗████╗ ██║╚══███╔╝██╔══██╗██║ ██╔════╝ ██╔═══██╗ ║
║ ██║ ███╗██║ ██║██╔██╗ ██║ ███╔╝ ███████║██║ ██║ ███╗██║ ██║ ║
║ ██║ ██║██║ ██║██║╚██╗██║ ███╔╝ ██╔══██║██║ ██║ ██║██║ ██║ ║
║ ╚██████╔╝╚██████╔╝██║ ╚████║███████╗██║ ██║███████╗╚██████╔╝╚██████╔╝ ║
║ ╚═════╝ ╚═════╝ ╚═╝ ╚═══╝╚══════╝╚═╝ ╚═╝╚══════╝ ╚═════╝ ╚═════╝ ║
║ ║
║ where does a formal library spend its axioms? ║
║ ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
#print axioms で分かるのは、ある定理が公理に依存しているかどうかです。公理が継承されたのではなく使われた箇所や、その影響がどこまで及ぶか、どれだけ回避できるか、あるいは特定の定理についてどのステップで導入されたかまでは分かりません。このツールなら分かります。
1つのプログラムで Lean 4 / Mathlib と Metamath のデータベース（set.mm、iset.mm、nf.mm）の両方に対応しているため、類推ではなく、同一の定義に基づいて2つの基礎体系を比較できます。
$ 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 を入力した行で一度警告を出します。しかし、その補題を使う3ファイル先の定理も未証明であることまでは警告しません。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 は、依存先を2種類に分けます。定義を命題で参照するものは、その意味が変更されます。一方、証明でのみ使うものは、再ビルドが必要になるだけです。
カーネル > sorry
発見された内容
Mathlib を含む Lean 4.32.1 を対象にすると、宣言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 ただ1つです。これは6つの補助補題の Decidable 引数に、ハードコードされた Classical.propDecidable を与え、インスタンス合成を試みません。そのため、Nat 上の a - b = 0 ↔ a ≤ b のような初等的な証明まで、必要のない選択公理に依存しています。上流に報告済みで、修正は1ファイルで済みます。
言語モデルに呼び出させる
$ pip install "gonzalgo[mcp]"
MCP クライアントの設定に追加します。
{
"mcpServers": {
"gonzalgo": { "command": "gonzalgo-mcp" }
}
}
10 個のツール：audit_trust、why、impact、axiom_reach、metamath_audit、
kernel_index、さらにプロジェクトからダンプを生成するための一連の機能があります。
また、gonzalgo にできないことを報告する scope ツールもあります。論文を読むこと、
宿題を採点すること、テキストの出来を判断することです。文章で書かれたページについて
「この証明は正しいですか？」と尋ねられたモデルが、手近にある証明らしきツールを
呼び出して無意味な結果を返さないようにするためのものです。それ以外の各ツールの説明には、
前提条件が明記されています。
想定されているのは、生成された Lean の証明がコンパイルに失敗する場合ではありません。
それなら簡単に見つけられます。問題なのは、3 つ上流の補題に sorry があるまま
コンパイルされる証明です。Lean はその箇所で、一度だけ、警告として言及します。
kernel_index はファイルもネットワークも使わずに実行されるため、既知のライブラリの
統計をモデルがすぐに取得できます。
CI に組み込んで、バッジを取得
Lean 4 プロジェクトなら、どれでも 3 行で設定できます。コミットごとに、未完成の証明や カーネルではなくコンパイラーを信頼している定理がないか検査します。
# .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 について警告します。しかし、3 つ先のファイルにある定理が
それをひそかに受け継いでいても、何も言いません。examples/dirty の実例では、Lean は
警告を1 件報告し、監査では汚染された定理が2 件見つかります。
仕組み
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
Kernel Trust Profile
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" }
]
}
大部分を左右するルールは 2 つです。測定されていないフィールドは null であり、0 ではありません。Metamath には native_decide がないため、compiler_trusted の数は 0 ではなく該当なしです。0 と書くと、誰もしていない主張になってしまいます。また、ツリーがダーティーな場合は revision が拒否されます。測定対象を示すコミットと一致しないプロファイルは、ほかの人が再現できないためです。
意図的に、要約スコアはありません。定理が未完了の証明に到達するかどうかは二択です。それをほかの何かと平均すると、測定にない精度を捏造することになります。
完全な仕様は Kernel Trust Profile 0.1（Zenodo）をご覧ください。サンプルは examples/lean-core-kernel-trust.json にあります。
到達範囲と増幅
インライン化や因数分解など、ライブラリの記述方法は変えても、証明する内容は変えない操作のもとでは、依存先の集合は不変ですが、エントリーポイントの集合は不変ではありません。公理の使用をすべて 1 つのゲートウェイ補題経由にしたり、その補題をインライン化したりすれば、定理を 1 つも変えることなく、増幅を 1 から依存先の数までの任意の値に移せます。
つまり、到達範囲はライブラリ間の比較に使えますが、増幅は 1 つのライブラリにおける因数分解を表します。 ツールは両方を報告し、この README ではそれぞれが何を指すのか説明しています。この違いは見失いやすく、見失った場合の代償も大きいためです。
知っておくべき落とし穴
Lean 4.32 では、ConstantInfo.value? は value? (allowOpaque := true) として呼び出さない限り、定理に対して 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
モジュールがインポートするものはすべて含まれ、5 列目の出力には各宣言の出所モジュールが記録されます。これにより、後からプロジェクトとその依存関係を区別できます。
ファイル内から呼び出す場合、ライブラリの利用は 2 行で済みます。
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。
Mathlib を使用した Lean 4.32.1 に適用すると（宣言数 790,171、依存関係の辺数 3,000 万）、Classical.choice への唯一の経路が置換可能な箇所を経由する宣言を 280 個見つけます。そのうち 276 個は、omega 判定手続きにおける単一の原因に起因します。280 個すべての証明項を書き換えてカーネルに提出した結果、276 個が受理され、4 個が拒否され、275 個で Classical.choice が不要になりました。
参照先
- keithadler/tenet — C#/.NET で実装された独立した Lean 4 カーネルチェッカーです。その
tenet whyは、どのステップで公理が導入されたかを追跡します。これは、Lean における gonzalgo の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 で、同梱データからすべての図を 1 つのコマンドで再生成できるアーカイブが付属しています。
- 形式ライブラリはどこで公理を使用するのか — 10.5281/zenodo.21769846
- タクティックレベルの割合では Lean の古典的依存関係を特定できない理由 — 10.5281/zenodo.21853489
ライセンス
Apache-2.0。LICENSE と NOTICE を参照してください。
OmegaFix.lean は Lean 4 の src/Lean/Elab/Tactic/Omega/Frontend.lean を改変したコピーです。Copyright (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 ║
║ ║
╚════════════════════════════════════════════════════════════╝
F-Keys の一部 — 独立系のハードウェア、ソフトウェア、インターネット製品です。作業ログとライブステータスをご覧ください。
コメント
AI アプリケーションが外部のツールやデータソースに統一的な方法で接続するためのオープンなプロトコルです。クライアントはモデルとの対話を担い、MCP サーバーはツール・リソース・プロンプトテンプレートを提供します。標準メッセージでやり取りするため、1 つのサーバーを複数のクライアントで再利用できます。