⏳ This skill is pending AI review.
Scores will appear once the review pipeline completes.
verify-and-repair-algebra
Check and repair rational polynomial identities with ResiMind when an expansion looks wrong, two algebraic answers disagree, or an agent needs exact coefficient evidence before using a result. Applies to bounded polynomial algebra, not calculus, arbitrary theorem proving or engineering certification.
Choose how to use this skill
You do not need every option. Choose the path your AI client supports. The stable page stays the same; versioned files are immutable.
1. Native installer
This listing has no registered native installer command. Use the complete package or source fallback below, depending on what your client supports.
Do not guess an installer command or replace an existing version without reviewing the diff.
2. Complete package recommended
Download the ZIP when available. It includes SKILL.md plus the references, security notes and version metadata.
No complete ProSkills package is published for this listing yet.3. Prompt-only
Copy the prompt above when the agent can read the stable page or when you want to adopt the workflow without installing a skill.
Need only the instruction file?
Download SKILL.md only if your client requires a single file. The complete ZIP is safer for a full installation because it preserves the references and release context.
No path installs or executes anything by itself. Your agent still needs access to the project files. Before updating, compare the installed version and review the diff.
// RATINGS
Not yet listed on ClawHub or SkillsMP
// README
ResiMind — Verified Memory for AI Agents
Catch the error. Keep the insight. Give the next task a checked head start.
Run the demo · Connect MCP · Install the Skill · Take the challenge · 中文
Frontier roadmap and evidence · External theorem benchmark boundary
Latest on main (after v0.16.0): memory provenance, expiry and transfer auditing, reserved revision steps in the ChinaTravel integration, and an experimental external Lean template compiler. The latest same-model planning result and development rerun are published with their failures; neither establishes a planning success-rate gain. MiniF2F and LeanDojo scores are still pending.
ResiMind is an open-source neuro-symbolic Agent architecture that connects independent verification, residual-guided self-correction and reusable rule memory. Your model, rules or symbolic tools propose a step; domain checks decide what becomes a fact. Failed checks tell the next attempt what still needs fixing.
A checked solution can become a checked rule. Explicit learning extracts candidate rules from completed derivations, independently verifies admission, and rechecks each future application. Knowledge grows outside the model, without changing its weights. When local rules or tools suffice, the supported math routes run with zero model calls.
Formal memory can now compose checked conditions. The bounded Lean planner introduces an implication, applies a verified conditional lemma, and sends the resulting residual subgoal to another verified lemma or a local assumption. The whole typed plan is compiled again by Lean; structural matching never counts as proof. This is an experimental composition primitive, not a claim of MiniF2F or general theorem-proving leadership.
The core also runs bridge engineering, constrained optimization, customer support and open-ended planning with their own verifiers. Adaptive algebra, rule learning and the five MCP tools currently cover bounded rational polynomials. Core: Python 3.10+, no runtime dependencies. Optional MCP: Python 3.11+.
| What you want to do | Your entry point |
|---|---|
| Give an existing Agent exact algebra tools | MCP setup · Download MCPB |
| Teach an Agent a bounded verify-and-repair workflow | Repair Skill · Install guide |
| Build an Agent with your own checks | Architecture · Adapter contract |
| Inspect what has actually been measured | Evidence · Release validation |
Created and originally published by @1105216375-alt. Citation · Changelog
Evaluating tools for your Agent? Make this one catch a wrong answer first. Run the nine-call integration probe: reject → repair → learn → recall, including an unsupported-scope control. No model key. Machine-readable cases · Documentation index
Try it in three minutes
With Python installed:
git clone https://github.com/1105216375-alt/resimind.git
cd resimind
python -m venv .venv
source .venv/bin/activate
python -m pip install .
python -m resimind demo --domain lifelong
On Windows PowerShell, activate with .venv\Scripts\Activate.ps1. Installation may download build tools. The demo runs offline, without an API key; both python -m resimind and the installed resimind command work outside the checkout.
The first demo solves two training problems, extracts a checked rule, saves and reloads frozen memory, and transfers that rule to new coefficients. It then solves a long expansion using a sparse certificate. The frozen memory stays unchanged throughout evaluation. No API calls are made.
Choose a different challenge. These commands run offline; the Lean example additionally requires an installed Lean 4.29.0 toolchain:
| Try | What the example makes visible | Command |
|---|---|---|
| Learning across episodes | Save and reload frozen memory, transfer a checked rule, and verify a long sparse expansion | python -m resimind demo --domain lifelong |
| Search and learning | Fit strategy preferences, extract checked schemas, and recheck only affected bridge cases | python -m resimind demo --domain search-learning |
| Goal progress | Skip a cosmetic rewrite, act on remaining expansion goals, and allow a useful step with a larger expression | python -m resimind demo --domain progress |
| Local scheduling | Reuse a useful rule, simplify before an expensive substitution, and skip model callbacks when local work suffices | python -m resimind demo --domain scheduling |
| Expression growth | Compare primitive expansion with bounded distribution and term collection on four quadratic factors | python -m resimind demo --domain growth-control |
| Lean proof feedback | A real unfinished Lean goal drives a new tactic, then a checked rule is reused | python -m resimind demo --domain lean |
| Adaptive reasoning | Reject a wrong step, change strategy, finish a proof and reuse its checked rule | python -m resimind demo --domain adaptive |
| Knowledge growth | Derive a rule, verify and store it, then reuse and recheck it on a new task | python -m resimind demo --domain knowledge-growth |
| General architecture extensions | Track dependent residual work, rank frozen strategies, and exact-check a reusable rule schema | python -m examples.general_architecture |
| Open-ended planning | Many valid answers; time, budget, and route constraints still apply | python -m resimind demo --domain planning |
| Customer support | A ¥259 refund proposal fails the configured ¥249 calculation | python -m resimind demo --domain customer-support |
| Mathematics | A lower objective is useless if the candidate violates a constraint; check an exact optimality certificate | python -m resimind demo |
| [Bridge engin |
// HOW IT'S BUILT
KEY FILES