math-frml-agen-patt

name	math-frml-agen-patt
description	Use when evaluating or absorbing ideas from math-formalization agents such as MathCode into Hermes workflows. Activate when a task involves theorem proving, reusable theorem/axiom stores, subgoal decomposition, proof planning, Lean feedback loops, or tool/skill/plugin split for math work.
tags	["math","theorem-proving","lean","agent-patterns","planning"]
version	1

Goal

• Reuse the transferable orchestration ideas from math-formalization agents without inheriting their whole runtime or trusting their bootstrap blindly.

Use this when

• A user shares a theorem-proving / Lean / formalization agent repo and wants the useful parts integrated.
• You need a structured way to plan proofs, decompose subgoals, or store reusable formal results.
• You want Hermes to reason about math workflows with explicit reusable artifacts.

Do not use this when

• The task is merely to install or run a third-party math agent; do security review first.
• The task is ordinary coding/debugging with no formalization workflow.

Core patterns to adopt

1. Tree of Subgoals
   • For hard proofs, decompose into explicit subgoals.
   • Prefer independent subgoals that can be checked separately.
   • Treat subgoal proof status as first-class state.
2. Guide of Plans
   • Generate multiple proof plans or attack strategies before committing.
   • Keep the planner distinct from the prover/executor.
3. Theorem Library
   • Reusable proved statements should be stored in a durable, queryable artifact.
   • Prefer canonical naming and append-only or auditable updates.
4. Axiom Library
   • Temporary assumptions must be explicit, named, and reviewable.
   • Never let assumptions hide inside free-form chat.
5. Tools / Skills / Plugins split
   • Skills encode method.
   • Tools perform deterministic checks/search/stats.
   • Plugins/integrations add optional surface area; do not bloat the core.
6. Structured feedback loop
   • Compiler/LSP/checker diagnostics should feed repair loops in structured form, not only raw stderr.

Hermes adaptation

• Do not install the external runtime unless the user asked for it.
• Absorb workflow ideas into skills and repo artifacts first.
• For theorem-style tasks:
  1. write the target statement
  2. list candidate plans
  3. decompose subgoals
  4. mark assumptions explicitly
  5. run deterministic checks
  6. store proved reusable lemmas/results in a durable artifact if the project has a formal store

Recommended artifacts

• DEBUG.md or PROOF.md for evidence trail
• docs/proof-plans/ for larger proof strategies
• project-local theorem/axiom stores when the repo already has them

Adoption filter

• Keep:
  • subgoal trees
  • reusable theorem/axiom stores
  • multi-plan search
  • structured tool/skill split
• Reject or weaken:
  • bootstrap installers as authority
  • hidden assumptions inside prompts
  • unconditional dependence on one vendor CLI/backend

Output pattern

• State what was absorbed: planning, subgoaling, theorem store, axiom discipline, or tool split.
• Name any explicit artifact or skill updated.

Pitfalls

• Do not treat assumptions as proved facts.
• Do not mix planner output and proof output without marking status.
• Do not let theorem libraries become unreviewed dump files.
• Do not force installation when workflow absorption is enough.