Execute qualquer Skill no Manus
com um clique

Execute qualquer Skill no Manus com um clique

numina-lean-agent

Estrelas20

Forks1

Atualizado23 de junho de 2026 às 19:19

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

Instalação

Instalar com Codex ou Claude Copie este prompt, cole no Codex, Claude ou outro assistente e deixe que ele revise a página da skill e instale para você.

Executar no Manus

Fonte

henryrobbins

henryrobbins/open-atp

Abrir repositório GitHub Ver repositórios do creator

Download

Executar no Manus

Ocupações relacionadasSOC

Baseado na classificação ocupacional SOC

Desenvolvedores de softwareInformática e Matemática·SOC 15-1252

Explorador de arquivos

35 arquivos

SKILL.md

readonly

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.)

Mais deste repositório

mesmo repositório

probe-skill

henryrobbins/open-atp

A no-op skill used only by the agent-capability tests to confirm a harness can mount and invoke a skill. Has no real behavior; invoke it when asked to during a capability probe.

2026-06-2320

lean4

henryrobbins/open-atp

Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, or learning Lean 4 concepts. Also trigger when the user asks for help with Lean 4, mathlib, or lakefile. Do NOT trigger for Coq/Rocq, Agda, Isabelle, HOL4, Mizar, Idris, Megalodon, or other non-Lean theorem provers.

2026-06-2320

code-transform

henryrobbins/open-atp

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

2026-06-2220

llm

henryrobbins/open-atp

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

2026-06-2220

henryrobbins/open-atp

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

2026-06-2220

sorrifier

henryrobbins/open-atp

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

2026-06-2220

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.)