neurocore-skill-math

A math-proof toolchain for NeuroCore: one package exposing many small, composable skills that wrap computer-algebra systems, SMT solvers, automated theorem provers, and formal proof assistants. A supervisor agent / FlowEngine blueprint composes them into proof-search and proof-validation chains.

pip install neurocore-skill-math          # pulls sympy, mpmath, z3-solver
pip install "neurocore-skill-math[cvc5]"  # + cvc5 SMT backend (optional)

Most external engines (Lean, Vampire, Isabelle, Coq, SageMath, GAP, PARI/GP, …) are not Python packages — install them with the provided script (scripts/install_math_tools.sh, Ubuntu 24.04) and check what's available:

# Check using python module or the installed CLI script
python -m neurocore_skill_math.check
neurocore-skill-math-check

Every skill detects whether its backend is installed and degrades gracefully (status tool_unavailable) rather than crashing a flow.

Skills

Result envelope & ports

Each skill writes a uniform envelope: {status, tool, available, result, log, error, duration_ms} with status ∈ {ok, proved, refuted, unknown, tool_unavailable, error, timeout}.

Skills set output ports so graph blueprints can route:

• SMT / Mace4: counterexample_found / no_counterexample
• ATP: proof_found / no_proof
• Lean/Isabelle/Coq check: verified / repair_needed / failed
• domain classifier: number_theory / group_theory / …

All skills take configurable input_key / output_key (the doc's dotted-key contract, e.g. evidence.sympy), so the same skill can be wired into different positions in a chain.

Blueprints

blueprints/ ships two reference proof workers from the design:

• lean-first-math-worker.flow.yaml — a focused parse → explore → refute → formalize → verify → repair → report loop.
• math-proof-validation-worker.flow.yaml — the full fan-out across CAS/SMT/ATP then Lean/Isabelle/Coq validation.

Graph routing. These workers use edge ports, edge conditions, and a Lean repair loop. With neurocore-ai>=0.4.0 (on flowengine>=0.6.0), NeuroCore routes such graph flows through flowengine's GraphExecutor, which honors port/condition gating and cyclic max_iterations — so the conditional early-exits and the repair loop execute as drawn. Plain DAGs (no ports/conditions/cycles) still use the concurrent layer executor. On older NeuroCore the skills' ports are simply ignored (all reachable nodes run).

Convention

Standard NeuroCore skill package: entry-point group neurocore.skills, import package neurocore_skill_math, kebab distribution neurocore-skill-math. See the skill-authoring guide.