Skip to content
Research
Skill

/code-transform

Code transformation tools for repairing, simplifying, and extracting Lean proofs

BOOST
@project-numinaproject-numina@project-numina
From plugin
numina-lean-agent
2825 skills
Install
$ npx -y skills add project-numina/numina-lean-agent --skill code-transform --agent claude-code

How it fires

How this skill gets triggered: by you, by Claude, or both.

  • Fires itselfAuto-invocation. Claude auto-loads it when your prompt matches the work.Auto-invocation is when the right skill fires by itself at the right moment, driven by a FLOW.md router and a hook, instead of you invoking it by name. It is the difference between a skill being installed and a skill actually getting used.Read the full definition →
  • You can call itInvoke it directly when you want it.
  • Slash command/code-transform

Context preview

The summary Claude sees to decide when to auto-load this skill.

Code transformation tools for repairing, simplifying, and extracting Lean proofs

SKILL.md

code-transform.SKILL.md
name: code-transform
description: "Code transformation tools for repairing, simplifying, and extracting Lean proofs"

Code Transform Tools

Tools for automatically transforming and improving Lean proof code. All scripts use `python skills/cli/axle.py <subcommand>`.

Available Tools

| Tool | Purpose | When to use | |------|---------|-------------| | **axle repair-proofs** | Auto-fix broken proofs using configurable repair strategies | When a proof fails and you want automated repair before manual editing | | **axle simplify-theorems** | Clean up proofs by removing unused tactics and bindings | As a final cleanup step after a proof is verified | | **axle sorry2lemma** | Lift sorry placeholders into standalone named lemmas | When a proof has multiple sorry sub-goals you want to tackle independently | | **axle extract-theorems** | Split a Lean file into structured per-theorem records | For analysis, dataset construction, or understanding file structure |

For full parameters and examples, read the corresponding `reference-<tool>.md` file in this directory.

Read it on GitHub ↗
Ships withnumina-lean-agent

Paper | Leandex | Demo | Putnam 2025 An agent built on Claude Code for formal theorem proving tasks. We used this system to prove all 12 problems from Putnam 2025, and completed a paper-level formalization of Effective Brascamp-Lieb inequalities.

Get the whole plugin
Stats
PythonBashGitGitHubAnthropic
+2 tags
OpenAIGemini
282
Stars
36
Forks
Maintained
Maintenance
Python
Language
3mo ago
Last commit
9mo ago
Created
5d ago
Added

Repo: project-numina/numina-lean-agent

In this plugin
5 skills
See everything inside

Other skills on numina-lean-agent.