/llm

LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification

BOOST

project-numina@project-numina

GitHub

From plugin

numina-lean-agent

2825 skills

Install

$ npx -y skills add project-numina/numina-lean-agent --skill llm --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.
You can call itInvoke it directly when you want it.
Slash command/llm

Context preview

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

LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification

SKILL.md

llm.SKILL.md

name: llm
description: "LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification"

LLM Tools

LLM-assisted tools for theorem proving support. All scripts are in `skills/cli/`.

Available Tools

| Tool | Purpose | When to use | |------|---------|-------------| | **informal-prover** | Generate and verify step-by-step math solutions in a loop | When you want an LLM to attempt a full solution with auto-verification | | **discussion-partner** | Free-form discussion about proof strategies or Lean code | When you are stuck and want high-level strategic advice | | **code-golf** | Shorten and simplify an existing Lean proof via Gemini | After a proof works, to get a more elegant version |

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

Python Bash Git GitHub Anthropic

+2 tags

OpenAI Gemini

282

Stars

Forks

Maintained

Maintenance

Python

Language