feat(skills): add axle lean 4 proof manipulation skill

[claudlos]

What does this PR do?

Adds a new skill for AXLE (Axiom Lean Engine) — a CLI and Python client for Lean 4 proof manipulation via the Axiom Math cloud API. This skill enables Hermes agents to verify proofs, check Lean code compilation, extract/merge/rename theorems, repair broken proofs, disprove statements, and normalize Lean files using 14 cloud-hosted tools — all without a local Lean installation.

AXLE is particularly useful for AI-driven formal verification workflows, Lean 4 + Mathlib development, and automated proof repair after library updates.

Type of Change

• New skill

Changes Made

• Added skills/mlops/evaluation/axle/SKILL.md (400 lines) — main skill document covering:
  • When to use AXLE vs alternatives (lean4checker, Comparator, SafeVerify, Pantograph)
  • Quick start with CLI and Python async client
  • 3 detailed workflows: proof verification, proof repair after Mathlib update, multi-file merge
  • Complete CLI reference for all 14 tools (validation, transformation, analysis, extraction, utility)
  • Python API overview with common usage patterns
  • 7 common issues with solutions
  • Advanced topics (security, metadata, HTTP API, error handling)
• Added skills/mlops/evaluation/axle/references/python-api.md (296 lines) — full Python API reference with all method signatures, response types, error hierarchy, helper functions, and environment variables
• Added skills/mlops/evaluation/axle/references/security.md (42 lines) — verify-proof security considerations, what AXLE blocks, verification error patterns, and recommended alternatives for untrusted code
• Added skills/mlops/evaluation/axle/references/extract-theorems-metadata.md (92 lines) — complete Document metadata reference with 20+ fields covering identity, content, proof complexity, 6 dependency lists, and compilation status
• Added skills/mlops/evaluation/axle/references/http-api.md (173 lines) — REST API reference with endpoints, authentication, request/response formats, error codes, and examples

How to Test

1. Install the skill: ensure skills/mlops/evaluation/axle/ is in the Hermes skills directory
2. Install the AXLE package: pip install axiom-axle
3. (Optional) Set API key: export AXLE_API_KEY=your_key
4. Test basic check:

   echo 'theorem foo : 1 + 1 = 2 := by norm_num' \
     | axle check --environment lean-4.28.0 --ignore-imports -

5. Test proof verification:

   echo 'theorem foo : 1 + 1 = 2 := by sorry' > /tmp/stmt.lean
   echo 'theorem foo : 1 + 1 = 2 := by norm_num' > /tmp/proof.lean
   axle verify-proof --environment lean-4.28.0 --ignore-imports /tmp/stmt.lean /tmp/proof.lean

6. Verify skill loads correctly: ask Hermes agent to "verify this Lean proof" and confirm it loads the AXLE skill

For New Skills

• SKILL.md follows standard format (YAML frontmatter with name, description, version, author, license, dependencies, tags)
• No unnecessary external dependencies (only axiom-axle PyPI package required)
• Tested end-to-end (CLI and Python API workflows verified against live Axiom Math API)
• Broadly useful to most users (if bundled) — this is a specialized skill for Lean 4 / formal verification workflows