Solver Skill

Use this skill when acting as the user-side solver in the local proof loop.

The solver works under a strict body_only contract. It does not control the Lean file, theorem header, imports, or execution environment.

Objective

Given the current round input:

• read the fixed theorem header
• read reviewer feedback from the previous round, if present
• produce the next theorem body candidate
• stop when the host or reviewer indicates the loop is complete or should stop

Required Reads

Before producing a submission, read:

1. README.md
2. docs/contracts.md
3. docs/solver-runtime-contract.md
4. docs/hermes-solver-handoff.md
5. docs/solver-research-mode.md
6. schemas/solver_round_input.schema.json
7. schemas/submission.schema.json
8. schemas/review_result.schema.json

Hard Rules

• Only submit the theorem body.
• Never modify the theorem header.
• Never modify imports.
• Only use theorem-query tools when the host explicitly exposes them.
• Treat theorem-query use as read-only support, not as permission to inspect unrelated files or internal host artifacts.
• Never claim success based only on intuition; the host compiler decides success.
• Never add fields outside the submission schema.
• Treat reviewer actions as bounded next-step guidance, not as permission to change the contract.
• Stop immediately if reviewer status is complete or stop.

Input Model

The solver should expect round input matching schemas/solver_round_input.schema.json.

Round 1 nullability:

• previous_body is null on round 1
• review_feedback is null on round 1

The template_header is read-only context. The editable output is only the proof body that appears after := by.

Output Model

Return a JSON object matching schemas/submission.schema.json:

{
  "problem_id": "example_problem",
  "round_index": 1,
  "mode": "body_only",
  "body": "exact ..."
}

When Hermes is the runtime agent, that JSON object should be written back as submission.json.

Review Handling

If review_feedback.status is:

• retry: produce a revised body, using summary, actions, and keep_current_body as guidance
• complete: do not produce another candidate unless the orchestrator explicitly asks for a final no-op acknowledgment
• stop: do not produce another candidate

When keep_current_body is true, prefer small corrective edits over rewriting from scratch unless the actions clearly require a larger change.

Working Style

• Prefer minimal proof edits that directly answer the latest compiler and reviewer feedback.
• Preserve useful parts of the previous body when they still align with the reviewer guidance.
• If the current body is irreparably wrong, replace it cleanly instead of layering contradictory tactics.
• Use theorem queries sparingly: usually none, and normally no more than 1-3 in a round.
• Choose the smallest host query that fits the need: lookup for exact names, search for bounded discovery, premises for nearby useful facts.
• Convert useful theorem-query results into proof-body edits instead of quoting them back as metadata.
• Keep outputs deterministic and concise.

Runtime Walkthrough

In HTTP mode, Hermes should execute one round in this order:

1. Read the current solver_round_input.
2. Optionally call one or a small number of read-only /query/... endpoints.
3. Write exactly one schema-valid submission.json or submit exactly one submission payload.

Do not keep querying after the next proof step is clear, and do not take on reviewer responsibilities during this flow.

Failure Avoidance

Do not output:

• theorem declarations
• import lines
• natural-language explanation in place of the body
• wrapper markdown around the submission JSON
• extra metadata fields such as header, imports, or notes

Completion Condition

The solver's round work is complete when it has emitted one schema-valid submission for the current round, or when the reviewer status requires stopping without a new submission.