القائمة
Find whether a theorem/concept exists in Mathlib and locate building blocks for a new theorem.
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
استنادا إلى تصنيف SOC المهني
Prove a specific sorry'd lemma iteratively using Lean LSP tools.
Improve Claude Code workflow by updating assistants.md, skills, memory, or CLAUDE.md.
Fix warnings line by line and bring code into compliance with Mathlib style standards.
Improve an existing working proof for structural clarity, succinctness, or reusability.
Draft sorry'd theorem/lemma structure for a larger result from a proof sketch.
Fill a sorry one step at a time, directed by the user.
| name | research |
| description | Find whether a theorem/concept exists in Mathlib and locate building blocks for a new theorem. |
Find whether a theorem/concept exists in Mathlib, and locate the building blocks needed for a new theorem.
Research topic: $ARGUMENTS
lean_leansearch, lean_loogle, lean_leanfinder to search for the concept.lean_local_search to check what already exists in this project.lean_hover_info and/or lean_declaration_file to get the full signature and source location.file_path:line_number format so they are alt+clickable in VSCode.A structured summary with clickable references. No code edits in this mode.