numina-lean-agent

name	numina-lean-agent
description	Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs

Numina Lean Agent — Skills Index

Skills

Skill	Description
search	Search tools: leanexplore, loogle, leanfinder, leansearch, state-search, hammer-premise
verification	Verification: lean-check, verify-proof, disprove
code-transform	Code transforms: repair-proofs, simplify-theorems, sorry2lemma, extract-theorems
llm	LLM tools: informal_prover, discussion_partner, code_golf

Environment variables

• GEMINI_API_KEY — informal_prover (gemini generation, gemini verifier, gemini refinement), code_golf, discussion_partner (gemini)
• OPENAI_API_KEY — informal_prover (gpt generation, gpt verifier), discussion_partner (gpt)
• ANTHROPIC_API_KEY — informal_prover (claude verifier)
• AXLE_API_KEY — axle commands (verify-proof, disprove, sorry2lemma, etc.)