ワンクリックでManusで任意のスキルを実行

math-identity-check

Numerically check whether two elementary-function expressions are equal. Use when someone asks "is sin(x)^2 + cos(x)^2 = 1?", "does log(x*y) equal log(x)+log(y)?", "verify this identity", "is this trig/log/algebraic identity true?", or when reviewing an LLM-generated proof, textbook answer, or student submission that asserts two closed-form expressions are equal. Handles sympy-parseable Python-style expressions and LaTeX (`\frac`, `\sqrt`, etc.). Produces a `verified` / `refuted` / `branch-dependent` / `cannot-verify` verdict with a concrete counterexample when the identity fails. Backs onto the EML proof engine when both sides compile to its witness library; falls back to sympy lambdify otherwise. NOT a symbolic proof — for that use sympy.simplify or a CAS.

Manusで実行

概要

インストールコマンド

npx skills add https://github.com/yaniv-golan/eml-skill --skill math-identity-check

このコマンドをClaude Codeにコピー＆ペーストしてスキルをインストール

ソース

yaniv-golan/eml-skill

スター1

フォーク0

更新日2026年4月19日 14:12

ファイルエクスプローラー

22 ファイル

SKILL.md

readonly

name	math-identity-check
description	Numerically check whether two elementary-function expressions are equal. Use when someone asks "is sin(x)^2 + cos(x)^2 = 1?", "does log(x*y) equal log(x)+log(y)?", "verify this identity", "is this trig/log/algebraic identity true?", or when reviewing an LLM-generated proof, textbook answer, or student submission that asserts two closed-form expressions are equal. Handles sympy-parseable Python-style expressions and LaTeX (`\frac`, `\sqrt`, etc.). Produces a `verified` / `refuted` / `branch-dependent` / `cannot-verify` verdict with a concrete counterexample when the identity fails. Backs onto the EML proof engine when both sides compile to its witness library; falls back to sympy lambdify otherwise. NOT a symbolic proof — for that use sympy.simplify or a CAS.
allowed-tools	Bash, Read, Write, Edit
license	MIT
metadata	{"author":"Yaniv Golan","version":"0.1.0"}

math-identity-check — numerically audit elementary identities

Two expressions in, one verdict out. Heavy lifting lives in skills/_shared/eml_core/identity.py; this skill is the user-facing entry point.

When this skill triggers

Triggers on: "is identity X true?", "does LHS equal RHS?", "verify sin(x)^2 + cos(x)^2 = 1", "check this trig identity", "is the LLM right that sqrt(x^2+y^2) = x+y?", "audit this step of a derivation".

Does not trigger on: requests for symbolic proof, simplification, or factoring (use sympy/CAS); requests to fit a formula from data (that's /eml-fit); requests to verify an EML tree specifically (that's /eml-check).

How to run

All commands below assume cwd is the repo root. From an installed plugin's root, drop the leading eml-skill/; from this skill's own directory, drop eml-skill/skills/math-identity-check/.

python eml-skill/skills/math-identity-check/scripts/check.py \
    --lhs "sin(x)**2 + cos(x)**2" \
    --rhs "1" \
    --out-dir ./

# refuted example — concrete counterexample returned:
python eml-skill/skills/math-identity-check/scripts/check.py \
    --lhs "sqrt(x**2 + y**2)" --rhs "x + y" --out-dir ./

# LaTeX also accepted:
python eml-skill/skills/math-identity-check/scripts/check.py \
    --lhs '\frac{\sin(2x)}{2}' --rhs 'sin(x)*cos(x)' --out-dir ./

Flags:

--lhs STR, --rhs STR — the two expressions. Python-style (x**2, sin(x)) or LaTeX (leading \ or containing \frac / \sqrt).
--domain NAME (default auto) — positive-reals, real-interval, complex-box, unit-disk-interior, right-half-plane, or auto (picked from the functions used).
--samples INT (1024) · --tolerance FLOAT (1e-10) · --seed INT (0).
--format json|md|all (default all) — identity.json + identity.md written into --out-dir.

Exit codes: 0 verified · 1 refuted · 2 branch-dependent · 3 cannot-verify · 4 parse-error.

Verdicts

verified — interior sample + branch-cut probes agree within tolerance.
refuted — interior mismatch; a concrete (x, y) counterexample is attached.
branch-dependent — interior matches but branch probes disagree (principal-branch–only identity). Example: log(x*y) vs log(x)+log(y) off the positive reals.
cannot-verify — one side contains a symbol, function, or construct we can't numerically evaluate.
parse-error — sympy couldn't parse one of the sides.

Output shape

identity.json + identity.md with: verdict, lhs / rhs side reports (sympy form, K and used_witnesses when EML-compilable, diagnostics), numerical (evaluator used: EML or sympy; domain, samples, tolerance, max_abs_diff), branch_flags, counterexample, caveats. Full schema in references/examples.md.

Gotchas

Numerical, not symbolic. "verified" means "agrees on N interior samples + branch probes within tolerance T." For formal proof, use sympy.simplify or Lean. Most LLM hallucinations fail numerically on the first sample.
Branch-dependent ≠ wrong. log(x*y) = log(x)+log(y) is true on the principal sheet for positive reals; off-axis it picks up a 2πi jump. The branch-dependent verdict preserves that nuance.
Free symbols other than x, y are rejected. Use substitution first. Constants allowed: e, pi, i.
Sampling is interior by default. Boundary checks happen via the branch-probe catalog; the sampler doesn't put points on cuts.
cannot-verify is honest, not a failure. If you see it, the identity might still be true — we just couldn't reduce it to something numerically evaluable.

Test scenarios

sin(x)^2 + cos(x)^2 == 1 → verified.
sqrt(x^2 + y^2) == x + y → refuted with counterexample.
log(x*y) == log(x) + log(y) → verified on positive reals; branch-dependent on complex-box.
2*sin(x)*cos(x) == sin(2*x) → verified.
z + 1 vs z - 1 → parse-error (z not in allowed symbols).

Non-goals

No symbolic simplification (use sympy).
No shorter-form search (use /eml-optimize).
No witness-library compilation report (use /eml-lab or /eml-check).

このリポジトリの他の Skills

同じリポジトリ

eml-check

yaniv-golan/eml-skill

Verify whether a claimed EML tree really computes a stated elementary function. Use when a user presents an EML expression (nested eml(...) form or RPN) and asks "does this really equal sin(x)?" / "is this a valid witness for log10?", when auditing proof-engine witness trees, when checking a compiler's output against a reference formula, or when someone needs a branch-cut / removable-singularity audit with an interior-domain sampler. Produces a structured audit report (audit.json, audit.md, audit.blog.md) covering leaf set, shape stats, numerical agreement, branch-cut flags, and removable-singularity caveats. The `--format blog` option emits a self-contained README/blog-friendly markdown artifact with embedded Mermaid, K-context table, witness provenance, and a probe table. Handles complex arithmetic via principal-branch cmath.

2026-04-191

eml-fit

yaniv-golan/eml-skill

Deterministic library-first regression — fit a CSV against the calculator-primitive witness library (unary, affine `a·w(x)+b` with constant snapping, depth-2 composite `w(v(x))`, binary `w(x,y)`) and emit a machine-checkable JSON verdict ranked by max |residual| and R². Use when you need a reproducible, audit-able answer to "which elementary law generated this data?" — the JSON output is downstream-consumable (no LLM in the loop), exit codes encode the verdict, complex-plane evaluation via cmath catches branch-cut hazards. Snaps to π, e, 1/ln(10), Catalan G, ζ(3), Khinchin K, log₂(e), e^π, γ, etc. Optional `--noise-sigma σ` for measured data; reports SE(a)/SE(b).

2026-04-191

eml-lab

yaniv-golan/eml-skill

Compile ordinary formulas (exp(x+y), x**y, ln(x*y), sin(x)+cos(x), sqrt(x*y), x/y, asin(x), atan(x), log10(x)) into EML trees, look up calculator-primitive witnesses (exp, ln, add, mult, sub, pow, neg, inv, div, pi, i, sin, cos, tan, sqrt, asin, acos, atan, log10), inspect arbitrary EML trees, or run one-shot compile-render to emit tree + diagram + audit + summary from a sympy expression. Use when a user wants to lower a sympy-parseable expression into the EML IR, ask "how many tokens does the mult witness take?", visualize a tree as Graphviz/Mermaid, convert between nested / RPN / JSON forms, read shape stats (K, depth, leaf histogram), or produce a shareable artifact bundle in one command. Every named elementary primitive has a stored tree; the only `needs_tree` entry is `apex` (the closure proof itself, not a callable primitive).

2026-04-191

eml-optimize

yaniv-golan/eml-skill

Verify numerical equivalence of two EML trees (interior samples + branch-cut probes), search for shorter trees via witness-swap peephole, or enumerate shortest trees bottom-up via beam search with function-hash deduplication, meet-in-the-middle complement lookup, backward goal-propagation priority population, and optional library-witness seeding. Use when a user wants to confirm two EML trees compute the same function, audit whether a subtree collapses to a known library entry (exp, ln, e, add, mult, sub, pow, neg, inv), or rediscover the shortest EML witness for a named claim (exp, ln, e, mult, sub, neg, inv, simple composites) within a K budget up to K=17. Produces delta-K, equivalence verdict with branch flags, or best-K tree with per-K candidate counts.

2026-04-191

eml-check

yaniv-golan/eml-skill

2026-04-191

eml-fit

yaniv-golan/eml-skill

2026-04-191

ソース

yaniv-golan

yaniv-golan/eml-skill

GitHub リポジトリを開く Creator のリポジトリを見る

インストールコマンド

ダウンロード

Manusで実行

役立つ用途SOC

数学者コンピュータ・数学職15-2021L4

name	math-identity-check
description	Numerically check whether two elementary-function expressions are equal. Use when someone asks "is sin(x)^2 + cos(x)^2 = 1?", "does log(x*y) equal log(x)+log(y)?", "verify this identity", "is this trig/log/algebraic identity true?", or when reviewing an LLM-generated proof, textbook answer, or student submission that asserts two closed-form expressions are equal. Handles sympy-parseable Python-style expressions and LaTeX (`\frac`, `\sqrt`, etc.). Produces a `verified` / `refuted` / `branch-dependent` / `cannot-verify` verdict with a concrete counterexample when the identity fails. Backs onto the EML proof engine when both sides compile to its witness library; falls back to sympy lambdify otherwise. NOT a symbolic proof — for that use sympy.simplify or a CAS.
allowed-tools	Bash, Read, Write, Edit
license	MIT
metadata	{"author":"Yaniv Golan","version":"0.1.0"}

math-identity-check — numerically audit elementary identities

Two expressions in, one verdict out. Heavy lifting lives in skills/_shared/eml_core/identity.py; this skill is the user-facing entry point.

When this skill triggers

How to run

All commands below assume cwd is the repo root. From an installed plugin's root, drop the leading eml-skill/; from this skill's own directory, drop eml-skill/skills/math-identity-check/.

python eml-skill/skills/math-identity-check/scripts/check.py \
    --lhs "sin(x)**2 + cos(x)**2" \
    --rhs "1" \
    --out-dir ./

# refuted example — concrete counterexample returned:
python eml-skill/skills/math-identity-check/scripts/check.py \
    --lhs "sqrt(x**2 + y**2)" --rhs "x + y" --out-dir ./

# LaTeX also accepted:
python eml-skill/skills/math-identity-check/scripts/check.py \
    --lhs '\frac{\sin(2x)}{2}' --rhs 'sin(x)*cos(x)' --out-dir ./

Flags:

--lhs STR, --rhs STR — the two expressions. Python-style (x**2, sin(x)) or LaTeX (leading \ or containing \frac / \sqrt).
--domain NAME (default auto) — positive-reals, real-interval, complex-box, unit-disk-interior, right-half-plane, or auto (picked from the functions used).
--samples INT (1024) · --tolerance FLOAT (1e-10) · --seed INT (0).
--format json|md|all (default all) — identity.json + identity.md written into --out-dir.

Exit codes: 0 verified · 1 refuted · 2 branch-dependent · 3 cannot-verify · 4 parse-error.

Verdicts

verified — interior sample + branch-cut probes agree within tolerance.
refuted — interior mismatch; a concrete (x, y) counterexample is attached.
branch-dependent — interior matches but branch probes disagree (principal-branch–only identity). Example: log(x*y) vs log(x)+log(y) off the positive reals.
cannot-verify — one side contains a symbol, function, or construct we can't numerically evaluate.
parse-error — sympy couldn't parse one of the sides.

Output shape

Gotchas

Numerical, not symbolic. "verified" means "agrees on N interior samples + branch probes within tolerance T." For formal proof, use sympy.simplify or Lean. Most LLM hallucinations fail numerically on the first sample.
Branch-dependent ≠ wrong. log(x*y) = log(x)+log(y) is true on the principal sheet for positive reals; off-axis it picks up a 2πi jump. The branch-dependent verdict preserves that nuance.
Free symbols other than x, y are rejected. Use substitution first. Constants allowed: e, pi, i.
Sampling is interior by default. Boundary checks happen via the branch-probe catalog; the sampler doesn't put points on cuts.
cannot-verify is honest, not a failure. If you see it, the identity might still be true — we just couldn't reduce it to something numerically evaluable.

Test scenarios

sin(x)^2 + cos(x)^2 == 1 → verified.
sqrt(x^2 + y^2) == x + y → refuted with counterexample.
log(x*y) == log(x) + log(y) → verified on positive reals; branch-dependent on complex-box.
2*sin(x)*cos(x) == sin(2*x) → verified.
z + 1 vs z - 1 → parse-error (z not in allowed symbols).

Non-goals

No symbolic simplification (use sympy).
No shorter-form search (use /eml-optimize).
No witness-library compilation report (use /eml-lab or /eml-check).