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.
git 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/commands/vince-gonzalez/gonzalgo/audit-lean-axioms)<a href="https://agentmods.dev/commands/vince-gonzalez/gonzalgo/audit-lean-axioms"><img src="https://agentmods.dev/badge/commands/vince-gonzalez/gonzalgo/audit-lean-axioms/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/commands/vince-gonzalez/gonzalgo/audit-lean-axioms"><img src="https://agentmods.dev/badge/commands/vince-gonzalez/gonzalgo/audit-lean-axioms.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.00025 | $0.00470 |
| Opus 5 | $0.00013 | $0.00235 |
| Sonnet 5 | $0.00005 | $0.00094 |
| Haiku 4.5 | $0.00003 | $0.00047 |
Grade A, and why
audit-lean-axioms 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 11d 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.
What it actually says
Use the lean-axiom-provenance skill to report what the Lean 4 project at
$ARGUMENTS rests on. That skill is the single source for the commands and, more
importantly, for how to read what they return — follow it end to end.
Order of work:
- Build the environment and generate a dump. Run
gonzalgo checkon it and do not proceed until it passes; a dump written withoutallowOpaquereads every theorem's proof as empty and every statement-versus-proof figure computed from it will be wrong rather than imprecise. gonzalgo trust— every theorem reaching asorryanywhere upstream, and everything carryingLean.ofReduceBool/Lean.ofReduceNat. Where you findsorryAx, say which kind it is: asorrysomebody typed, or a proof that failed to elaborate and was admitted anyway. If you cannot tell them apart from the evidence, say that instead of guessing.gonzalgo eligible— the ceiling on removable classical dependence. Report it as a ceiling. A theorem with a choice-free statement can still need excluded middle.- For anything notable,
gonzalgo whyon the specific declaration, and quote the labelled path rather than paraphrasing it.
Honor a --axiom in $ARGUMENTS if one is given; the default target is
Classical.choice.
Finish with a plain verdict — CLEAN / INHERITED-SORRY / COMPILER-TRUSTED / CLASSICAL-ONLY — the counts behind it, and the exact Lean and Mathlib versions measured. A count with no version attached goes stale silently.
Do not call a proof wrong because it depends on Classical.choice. Nearly all of
Mathlib does, and for most theorems the statement requires it. The finding worth
reporting is dependence the proof introduced.
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.
- 11d ago First seen · 37 lines · 25 tokens per session scan A df0c7e6f1262
audit-lean-axioms is a command published in the GitHub repository vince-gonzalez/gonzalgo (2 stars, last pushed yesterday), licensed Apache-2.0. It adds 25 tokens to every session and 470 once invoked, about $0.0001 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 commands, from other repositories
brainblast-deploy-plan
Deployment Intelligence for Anchor programs. Run before anchor deploy so you know how much SOL you need and the exact ordered transaction sequence — instead of working it out by hand.
brainblast-oracle
Live On-Chain Intelligence: is the oracle fresh? Before you price anything against a Pyth / Switchboard / Chainlink feed, check when its account was last written.
brainblast-rico-maps
Runs a two-part token check on any Solana contract address (CA).
costguard-live
Plan and ingest an opt-in, consent-gated live billing check for a provider, conducted via the playwriter MCP server (read-only browser reads over your logged-in session). costguard never drives the browser itself.
proofrag
Evaluate a RAG/LLM app — generate a golden set, judge it, and produce a scorecard.
goal-audit
Attack the goal's own acceptance criteria — ledger integrity, negative control, and mutation probe (does not consume an iteration).