메뉴
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.
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
SOC 직업 분류 기준
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.
Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs
Code transformation tools for repairing, simplifying, and extracting Lean proofs
LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
Search tools for finding Lean theorems, lemmas, and definitions in Mathlib
Isolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple complex Lean 4 proofs.
| name | probe-skill |
| description | 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. |
This skill exists solely so the capability suite can verify that the skill a
harness's configure_wd mounts is discoverable and invocable inside the sandbox.
It does nothing. If you have invoked it, the capability check has already passed — stop immediately and make no further tool calls.
