Plugin Claude Code
Find out what a Lean 4 project rests on and why — inherited sorry, nativedecide, and which step introduced an axiom, with statement dependencies kept apart from proof dependencies.
Command
Report what a Lean 4 project rests on — inherited sorry, nativedecide, and where its axiom dependence comes from.
Command
Explain why a Lean declaration depends on an axiom, and whether that dependence could be rerouted.
Skill Claude CodeCodex
Find out what a Lean 4 project actually rests on, and why. Reports every theorem reaching a sorry anywhere upstream, everything settled by nativedecide rather than the kernel, and the shortest path from any declaration to any axiom with each hop labelled a statement dependency or a proof dependency. Use when the user…
Skill Claude CodeCodex
Check whether a machine-generated Lean 4 proof actually proves its theorem. A proof can appear in the environment, pass lake build, and still not have been proved: when elaboration fails Lean admits the declaration carrying sorryAx, which an axiom report cannot tell apart from a sorry somebody typed. Use when auditing…
MCP server Claude CodeCodexCursor
Measure where a formal library spends its axioms: Lean 4 and Metamath. Runs locally from the gonzalgo Python package.