القائمة
Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs
يُحدَّد Prompt الذي يراجع المصدر أولًا بشكل افتراضي. يمكنك التبديل إلى أمر مباشر أو تنزيل نسخة محلية.
اقرأ SKILL.md وأي ملفات مرافقة يعرضها SkillsMP قبل أن تقرر التثبيت.
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
يتجاوز الأمر المباشر Prompt المخصّص للمراجعة. افحص المصدر قبل تشغيله.
npx skills add https://github.com/project-numina/numina-lean-agent --skill numina-lean-agentيبقى الأمر في سطر واحد. مرّر أفقيًا لمراجعته كاملًا قبل النسخ.
تفضّل نسخة محلية؟ نزّل الملفات المتاحة حاليًا لدى SkillsMP.
استنادا إلى تصنيف SOC المهني
عرض SKILL.md
| name | numina-lean-agent |
| description | Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs |
| 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 |
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.)