Menu
Background knowledge for symproof — deterministic proof writing with SymPy. Apply when working in this repo.
Instalar com Codex ou Claude Copie este prompt, cole no Codex, Claude ou outro assistente e deixe que ele revise a página da skill e instale para você.
Construct a proof for a framed hypothesis — build lemma chains, import library proofs, seal into a bundle. Use when an engineer needs to prove a specific property.
Audit proof bundles — verify correctness, assess coverage, find gaps. Use when reviewing proofs for a system's requirements.
Frame proof problems — define axioms and hypotheses for a system. Produces the problem statements, not the proofs. Use when a domain expert wants to state what needs to be proven.
Baseado na classificação ocupacional SOC
| name | symproof-base |
| description | Background knowledge for symproof — deterministic proof writing with SymPy. Apply when working in this repo. |
| user-invocable | false |
symproof is designed for collective coverage — many small, focused proofs that each address one property of a system. This is more powerful and more scalable than complex proofs that try to establish everything at once.
A single system should have MANY independent proofs:
Each proof is sealed independently with its own hash. The hashes go into a requirements traceability matrix — each proof hash maps to a specific requirement. A reviewer can verify any proof independently without understanding the others.
Composition via import_bundle is for when one property LOGICALLY DEPENDS on another (e.g., uniqueness depends on strict convexity). It is NOT for bundling unrelated properties together. If stability and controllability are independent properties, prove them separately.
symproof covers the symbolic analysis layer only. It does not replace simulation (Monte Carlo, HIL) or code verification (static analysis, formal methods). A complete V&V program needs all three layers, with symproof's proof hashes linking the symbolic layer to the requirements alongside simulation results and audit findings.
AxiomSet → axiom_set_hash
→ Hypothesis (carries axiom_set_hash)
→ ProofScript (carries axiom_set_hash + imported_bundles + lemmas)
→ verify_proof(script) → ProofResult
→ seal(axiom_set, hypothesis, script) → ProofBundle(bundle_hash)
seal() is the ONLY path to a ProofBundle. It enforces:
foundations= is provided, every axiom in each foundation's axiom set must exist in the downstream axiom set (hidden axiom enforcement)simplify(axiom.expr) must not be False (checked at AxiomSet construction)check_consistency=False to skip)Symbol("x", positive=True)) that affect lemma verification must be declared as axioms| Kind | Checks | Use when |
|---|---|---|
| EQUALITY | simplify(expr - expected) == 0, .doit() fallback | Algebraic identities, series, closed forms |
| BOOLEAN | simplify → refine → proof-by-contradiction | Implications, inequalities, relational |
| QUERY | sympy.ask(expr, Q-context) | Positivity, type predicates (irrational, integer) |
| PROPERTY | getattr(expr, property_name) is truthy | Topological/structural properties (is_open, is_closed) |
| INFERENCE | depends_on non-empty + rule non-empty | Logical conclusions from premises (Heine-Borel, duality) |
| COORDINATE_TRANSFORM | Round-trip + transform + simplify/trigsimp | Polar, hyperbolic, body-frame transforms |
Results carry advisories: tuple[str, ...] when verification passes through known SymPy limitations. Every advisory is a flag for human review — it doesn't mean the proof is wrong, it means an engineer should inspect this step.
Use import_bundle ONLY when there is a logical dependency between proofs. The imported bundle's proof is re-verified at seal time.
# YES: uniqueness depends on strong convexity
unique = unique_minimizer(axioms, f, vars, m) # internally imports strongly_convex
# NO: don't bundle unrelated properties
# Instead: prove stability and controllability SEPARATELY, trace both to requirements
max_ge_first(ax, a, b) — Max(a,b) >= apiecewise_collapse(ax, expr, cond, fb, assumptions) — Piecewise branch collapsehurwitz_second_order / hurwitz_third_order — Routh-Hurwitzclosed_loop_stability(ax, G_n, G_d, C_n, C_d, s) — plant+controller → Hurwitzlyapunov_stability(ax, A, P, Q) — verify given Lyapunov equationlyapunov_from_system(ax, A) — CONSTRUCT P and prove PDgain_margin(ax, coeffs, K, s) — gain below criticalcontrollability_rank(ax, A, B) — Gramian det ≠ 0observability_rank(ax, A, C) — Gramian det ≠ 0quadratic_invariant(ax, states, dots, V) — dV/dt = 0envelope_theorem(ax, f, x, theta) — prove dV/dtheta = df/dtheta|_{x*} for strongly concave fconvex_scalar / convex_hessian / strongly_convex — convexity proofsconjugate_function — compute and verify Fenchel conjugateconvex_sum / convex_composition — DCP composition rulesunique_minimizer — strictly convex → unique (imports strongly_convex)gp_to_convex — geometric program log-transformconstant_acceleration / rotational_kinematic — kinematic equations via differentiationshm_solution_verify / shm_energy_conservation — SHM ODE and energy conservationwork_energy_theorem / impulse_momentum — work-energy, impulse-momentumgravitational_potential_from_force — U(r) from F(r)feasible_point / dual_feasible — LP primal and dual feasibilitystrong_duality / complementary_slackness — duality conditionslp_optimal — composed: primal + dual + duality => optimalinteger_feasible / lp_relaxation_bound — ILP feasibility and relaxation boundsverify_open / verify_closed / verify_compact — set properties (uses PROPERTY kind)verify_boundary / continuous_at_point — boundary and continuityintermediate_value / extreme_value — IVT and EVTgate_truth_table / circuit_equivalence — gate verificationcircuit_output / circuit_satisfies — circuit evaluationr1cs_witness_check — ZK-SNARK witness satisfactionboolean_entropy — output entropy (information leakage)entropy / joint_entropy / mutual_information — entropy measureskl_divergence — KL divergence with Gibbs' inequalitybinary_entropy_func / binary_symmetric_channel — channel theoryfee_complement_positive — 1-f > 0 from bounded intervalamm_output_positive / amm_product_nondecreasing — AMM propertiesmul_down / mul_up / div_down / div_up — directed roundingrounding_bias_lemma / rounding_gap_lemma / chain_error_bound — error analysisphantom_overflow_check / no_phantom_overflow_check — uint256 safetyunevaluated() and evaluation()SymPy eagerly evaluates expressions at construction time — Symbol("x", positive=True) > 0 becomes True, losing the structural information. symproof inverts this:
unevaluated() — suppress eager evaluation during axiom/expression constructionevaluation() — explicit gate around simplify(), ask(), refine()Best practice: always build axiom sets under unevaluated():
from symproof import unevaluated
with unevaluated():
axioms = AxiomSet(name="system", axioms=(
Axiom(name="x_pos", expr=x > 0), # stays structural, not True
))
All simplify()/ask()/refine() calls in verification.py, bundle.py, tactics.py, and library functions are wrapped in evaluation() gates. This makes every evaluation point explicit and auditable.
Inherited axioms must carry a Citation for traceability:
from symproof import Citation
Axiom(
name="bounded_gradient",
expr=gamma > 0,
inherited=True,
citation=Citation(source="Flam 2004, Theorem 2"),
)
Citation has two fields:
source: str — human-readable reference (required)bundle_hash: str = "" — optional link to a foundation ProofBundleThe hidden axiom problem is a major cause of failures in applied mathematics. When a proof cites an external theorem, it inherits that theorem's assumptions. If those assumptions are not explicitly declared and verified for the specific application, the proof has a soundness gap.
Example: a convergence proof cites Flam's stochastic heavy ball theorem. Flam's theorem requires bounded stochastic gradients, a Lipschitz-continuous objective, and Robbins-Monro step sizes. If the downstream proof only declares "Flam's theorem holds" without carrying these conditions, it has three hidden axioms.
seal(foundations=...)foundation = make_convergence_bundle() # proves theorem under its own axioms
bundle = seal(axioms, hypothesis, script,
foundations=[(foundation, "convergence_theorem")])
# ValueError if foundation.axiom_set has axioms missing from `axioms`
Add the foundation's conditions to the downstream axiom set with inherited=True:
Axiom(name="bounded_gradient", expr=gamma > 0, inherited=True,
citation=Citation(source="Flam 2004, Theorem 2"),
description="Required by convergence theorem foundation.")
inherited=True means: "this condition was not a design choice — the proof chain forced it." Both posited and inherited axioms are required for soundness, but the distinction traces provenance. The citation is required on all inherited axioms — it records where the condition came from.
Use seal(foundations=...) whenever:
expr=sympy.S.true and a separate proof backs itSee symproof/library/examples/dip_routing/ for a complete worked example where foundation enforcement revealed 7 hidden axioms across 3 proof pairs.
0 < f < 1 → 1-f > 0. Workaround: helper symbol g = 1-f.