메뉴
Use when preparing optional AxiomMath AXLE MCP setup for manual formal-proof assistance.
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
SOC 직업 분류 기준
Single-agent paper review workflow.
Comprehensive guide and reference for the Antigravity Customization System. Use to explain how customizations work, their loading priority, discovery mechanisms, and to guide the creation of skills, rules, plugins, hooks, and MCP servers.
Provides a comprehensive guide, quick reference, and sitemap for Google Antigravity (AGY), including the Antigravity CLI (agy), Antigravity 2.0, Antigravity IDE, Python SDK, slash commands, keybindings, and customizations (skills, rules, MCP, sidecars). Activate this skill when the user asks questions about how to use, configure, or customize Antigravity, AGY, the agy CLI, the Antigravity IDE, or Antigravity 2.0.
Guidelines for interacting with GitHub and request permissions from the user when commands fail due to restrictions in the agent environment.
ALWAYS use this skill when the user asks to send, get, retrieve, find, share, add, or search for a paper. This skill manages the user's Zotero library with 10,000+ papers and can retrieve PDFs, create share links, add new papers, and search. Prefer this over getscipapers for any request involving sending/getting/finding papers.
Use when the user asks to send, get, retrieve, find, share, add, or search for a paper. This is the live OpenClaw Zotero workflow adapted for Codex and should take priority over external paper retrieval.
| name | axiom-axle-mcp |
| description | Use when preparing optional AxiomMath AXLE MCP setup for manual formal-proof assistance. |
This skill is installed as an OpenCode-native SKILL.md. For runtime-backed
helpers, prefer the shared ai-agents-skills runtime root and the
AAS_RUNTIME_ROOT override instead of assuming a Codex-specific runtime
path.
On native Windows, use the managed Windows runner and the native runtime command target. Set $runtime to the installed runtime root. Multi-agent installs usually use %LOCALAPPDATA%\ai-agents-skills\runtime. Then run:
$runtime = if ($env:AAS_RUNTIME_ROOT) { $env:AAS_RUNTIME_ROOT } else { "$env:LOCALAPPDATA\ai-agents-skills\runtime" }
& "$runtime\run_skill.bat" "skills/axiom-axle-mcp/run_axiom_axle_mcp.bat" doctor
PowerShell runner target:
& "$runtime\run_skill.ps1" "skills/axiom-axle-mcp/run_axiom_axle_mcp.ps1" doctor
POSIX examples below use run_skill.sh and .sh command targets; use the Windows command target above on native Windows.
Use this skill only for explicit optional AXLE MCP setup. It never installs packages, starts an MCP server, writes MCP/client config, stores credentials, or calls AxiomMath services. It reports local readiness and emits manual configuration snippets with placeholders.
Check local readiness without running uvx:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/axiom-axle-mcp/run_axiom_axle_mcp.sh doctor
Emit a manual MCP config snippet:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/axiom-axle-mcp/run_axiom_axle_mcp.sh config-snippet
Run offline smoke:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/axiom-axle-mcp/run_axiom_axle_mcp.sh smoke
The emitted local stdio snippet uses command uvx and args ["--from", "axiom-axle-mcp==0.3.3", "axle-mcp-server"] with placeholder <AXLE_API_KEY>. The hosted URL https://mcp.axiommath.ai/mcp is manual setup only.
AXLE output is remote supplemental evidence. Record it as axle_remote_check, never as formal_check. It cannot set local lean_check_status, satisfy placeholder or trust-base scans, replace statement-equivalence review, or promote formal support without local Lean/project evidence.