Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add vince-gonzalez/gonzalgo --skill lean-generated-proof-auditgit clone --depth 1 https://github.com/vince-gonzalez/gonzalgoWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/vince-gonzalez/gonzalgo/lean-generated-proof-audit)<a href="https://agentmods.dev/skills/vince-gonzalez/gonzalgo/lean-generated-proof-audit"><img src="https://agentmods.dev/badge/skills/vince-gonzalez/gonzalgo/lean-generated-proof-audit/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/vince-gonzalez/gonzalgo/lean-generated-proof-audit"><img src="https://agentmods.dev/badge/skills/vince-gonzalez/gonzalgo/lean-generated-proof-audit.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00143 | $0.01619 |
| Opus 5 | $0.00072 | $0.00809 |
| Sonnet 5 | $0.00029 | $0.00324 |
| Haiku 4.5 | $0.00014 | $0.00162 |
Grade A, and why
lean-generated-proof-audit scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 10d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 143 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Auditing machine-generated Lean proofs
Compilation is not verification. This is established — SorryDB (arXiv 2603.02668),
AXLE (arXiv 2606.26442) and Faults in Our Formal Benchmarking (arXiv 2606.29493)
all say so, and the last recommends checking #print axioms output. What the
field has not published is how much difference the check makes.
One measurement exists. Over 10,000 Goedel-Prover outputs on the Lean Workbook
problems, 560 were admitted into the environment carrying sorryAx — present,
counted by a naive compile check, not proved. With 1 unparsable header and 270
that never entered the environment, 831 of 10,000 are excluded and the real
denominator is 9,169.
Setup
pip install gonzalgo
gonzalgo lean-files ./scripts
lake build
lake env lean -D maxErrors=4000 scripts/Split.lean # -> dump.tsv
gonzalgo check dump.tsv
gonzalgo check is not optional. ConstantInfo.value? returns none for theorems
unless passed allowOpaque := true, and an extractor written the obvious way reads
every proof as empty while reporting statement figures as proof figures.
-D maxErrors=4000 must be on the command line; set_option maxErrors inside a
file is ignored, and a generated corpus produces errors early and often.
The audit
1. Establish the denominator before anything else.
Count what entered the environment, what failed to parse, and what carries
sorryAx. Those three are different populations and mixing them is how a pass
rate gets overstated. Report the corpus size, the excluded count with its reasons,
and the number that actually compiled — and check that they sum.
gonzalgo trust dump.tsv
2. Separate the three outcomes of a failed proof.
Lean's sorry is implemented by sorryAx, and the elaborator emits a synthetic
one when a tactic fails to close a goal or an expression fails to typecheck.
- A
sorryin the source. In the environment, carryingsorryAx. - A failed elaboration that was admitted anyway. Also in the environment, also
carrying
sorryAx, and identical to case 1 in an axiom report. - A failure whose declaration never entered the environment. Invisible to an axiom report, because there is nothing there to report on.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 10d ago First seen · 143 lines · 143 tokens per session scan A 56009b4b80b1
lean-generated-proof-audit is a skill published in the GitHub repository vince-gonzalez/gonzalgo (2 stars, last pushed 7d ago), licensed Apache-2.0. It adds 143 tokens to every session and 1,619 once invoked, about $0.0007 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-31.
Other skills, from other repositories
automatic-differentiation-advanced
Extend Sounio's automatic differentiation capabilities to higher‑order derivatives, Hessians, differentiation through control flow, and GPU‑accelerated gradient computation, enabling state‑of‑the‑art scientific machine learning.
epistemic-uncertainty-quantification
Extend Sounio's epistemic types with advanced uncertainty quantification methods, such as confidence intervals, non‑Gaussian distributions, and Dempster‑Shafer evidence combination, positioning the language at the state‑of‑the‑art in measurement science.
formal-verification-epistemic
Integrate formal verification tools (SMT solvers, Lean) to prove properties of epistemic programs, such as uncertainty bounds, confidence guarantees, and provenance integrity, establishing Sounio as a language with mathematically verified scientific claims.
Academic Writing
Rewrite research prose to be clear, concise, precise, and appropriately cautious.
Citation Checking
Check whether citations support empirical claims and flag unsupported statements.
Literature Review
Compare related papers and organize prior work into a clear research narrative.