project-numina

project-numina/numina-lean-agent

Instructions file

Claude Code instructions for project-numina/numina-lean-agent, covering numina lean agent, lean environment and environment variables.

project-numina/numina-lean-agent

Plugin Claude Code

Lean 4 theorem proving tools: search, verification, LLM-assisted proving.

project-numina/numina-lean-agent

Skill Claude CodeCodex

Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs.

project-numina/numina-lean-agent

Skill Claude CodeCodex

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

project-numina/numina-lean-agent

Skill Claude CodeCodex

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

project-numina/numina-lean-agent

Skill Claude CodeCodex

Search tools for finding Lean theorems, lemmas, and definitions in Mathlib.

project-numina/numina-lean-agent

Skill Claude CodeCodex

Isolates failing proof steps by replacing them with sorry and extracting them into standalone lemmas to modularize and decouple complex Lean 4 proofs.

project-numina/numina-lean-agent

Skill Claude CodeCodex

Verification tools for compiling, validating, and disproving Lean theorems.

project-numina/lean-lsp-mcp

MCP server Claude CodeCodexCursor +2

Lean Theorem Prover MCP. Runs locally from the lean-lsp-mcp Python package.