Certificate coverage
DerivedResult.certificate returns Lean 4 source only where the emitter can prove the statement without sorry. This page is the map of that boundary. It is generated by running a corpus and recording what actually emitted — never hand-maintained — from tests/lean_corpus.py (the strict, CI-typechecked corpus) and tests/textbook_gate/ (first-course calculus and algebra). tests/lean_tendsto_corpus.py contributes the recognised Filter.Tendsto fragment (x → +∞, x → 0, finite). tests/lean_gosper_corpus.py contributes Gosper Finset.sum telescopes and the ∏ k = n! product identity.
Corpus: 332 observations over 208 shape classes — 117 certified, 2 conditional, 0 partial, 89 withheld.
Reading a row
A shape class is an operation plus a structural fingerprint of its arguments: which primitive functions occur (funcs), whether they are applied to the bare variable, to an integer power of it, or to something else (fn_arg), what kinds of exponents appear (pow, pow_base), how factors combine (mul), and the top-level form of the expression (form).
| Verdict | Meaning | certifiable() |
|---|---|---|
| ✅ certified | every corpus observation emitted a certificate | True |
| 🟡 conditional | emits when the operation rewrites something; some observations had an empty derivation log | False (class_conditional) |
| 🟠 partial | observations disagree — the class is too coarse to separate them | False (class_partial) |
| ⛔ withheld | no observation ever certified | False (class_withheld) |
certifiable() answers True only for certified classes, and in its default verify mode confirms by running the operation before saying so. It under-claims by construction: a shape the corpus has never reached answers False with reason unknown_shape.
diff
76 shape classes — 49 certified, 27 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | form=apply, funcs=Ei, fn_arg=var, mul=none, pow=none, pow_base=none | Ei(x) | diff_primitive_registry |
| ⛔ withheld | form=apply, funcs=Si, fn_arg=var, mul=none, pow=none, pow_base=none | Si(x) | diff_primitive_registry |
| ✅ certified | form=apply, funcs=asin, fn_arg=var, mul=none, pow=none, pow_base=none | asin(x) | — |
| ✅ certified | form=apply, funcs=atan, fn_arg=var, mul=none, pow=none, pow_base=none | atan(x) | — |
| ⛔ withheld | form=apply, funcs=atan2, fn_arg=other, mul=none, pow=none, pow_base=none | atan2(x, 1) | diff_primitive_registry |
| ✅ certified | form=apply, funcs=cos,sin, fn_arg=other, mul=none, pow=none, pow_base=none | sin(cos(x)) | — |
| ✅ certified | form=apply, funcs=cos, fn_arg=other, mul=scalar, pow=none, pow_base=none | cos((2 * x)) | — |
| ✅ certified | form=apply, funcs=cos, fn_arg=pow, mul=none, pow=nat, pow_base=var | cos(x^2) | — |
| ✅ certified | form=apply, funcs=cos, fn_arg=var, mul=none, pow=none, pow_base=none | cos(x) | — |
| ✅ certified | form=apply, funcs=cosh, fn_arg=var, mul=none, pow=none, pow_base=none | cosh(x) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=other, mul=scalar, pow=nat, pow_base=var | exp((-1 * x^2)) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=other, mul=scalar, pow=none, pow_base=none | exp((-1 * x)) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=pow, mul=none, pow=nat, pow_base=var | exp(x^2) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=var, mul=none, pow=none, pow_base=none | exp(x) | — |
| ⛔ withheld | form=apply, funcs=log,sqrt, fn_arg=other, mul=none, pow=nat, pow_base=var | log((sqrt((-1 + x^2)) + x)) | diff_log, diff_sqrt, sum_rule |
| ✅ certified | form=apply, funcs=log, fn_arg=var, mul=none, pow=none, pow_base=none | log(x) | — |
| ✅ certified | form=apply, funcs=sin, fn_arg=pow, mul=none, pow=nat, pow_base=var | sin(x^2), sin(x^3) | — |
| ✅ certified | form=apply, funcs=sin, fn_arg=var, mul=none, pow=none, pow_base=none | sin(x) | — |
| ✅ certified | form=apply, funcs=sinh, fn_arg=var, mul=none, pow=none, pow_base=none | sinh(x) | — |
| ⛔ withheld | form=apply, funcs=sqrt, fn_arg=other, mul=none, pow=nat, pow_base=var | sqrt((1 + x^2)) | diff_sqrt |
| ✅ certified | form=apply, funcs=sqrt, fn_arg=var, mul=none, pow=none, pow_base=none | sqrt(x) | — |
| ✅ certified | form=apply, funcs=tan, fn_arg=var, mul=none, pow=none, pow_base=none | tan(x) | — |
| ✅ certified | form=apply, funcs=tanh, fn_arg=var, mul=none, pow=none, pow_base=none | tanh(x) | — |
| ✅ certified | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none | 7 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var | x^10, x^2, x^3 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=neg, pow_base=var | x^-2 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=neg_one, pow_base=var | x^-1 | — |
| ✅ certified | form=power, funcs=sin, fn_arg=var, mul=none, pow=nat, pow_base=expr | (sin(x))^2 | — |
| ✅ certified | form=power, funcs=sin, fn_arg=var, mul=none, pow=neg_one, pow_base=expr | (sin(x))^-1 | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=expr | ((1 + x)^-1 * x) | power_rule, product_rule |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=frac, pow_base=expr | ((x^(1/2))^3 * 2/3) | power_rule, product_rule |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=nat, pow_base=var | (1/4 * x^4), (1/5 * x^5) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=expr | ((-1 + x)^-1 * -1) | power_rule, product_rule |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=var | (-1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=atan, fn_arg=other, mul=scalar, pow=none, pow_base=none | (1/2 * atan((1/2 * x))) | diff_primitive_registry, product_rule |
| ✅ certified | form=product, funcs=cos,exp, fn_arg=var, mul=general, pow=neg_one, pow_base=expr | ((cos(x))^-1 * exp(x)) | — |
| ⛔ withheld | form=product, funcs=cos,log, fn_arg=other, mul=scalar, pow=none, pow_base=none | (-1 * log(cos(x))) | diff_log, product_rule |
| ✅ certified | form=product, funcs=cos,sin, fn_arg=var, mul=general, pow=neg_one, pow_base=expr | ((cos(x))^-1 * sin(x)) | — |
| ✅ certified | form=product, funcs=cos,sin, fn_arg=var, mul=general, pow=none, pow_base=none | (cos(x) * sin(x)) | — |
| ✅ certified | form=product, funcs=cos, fn_arg=other, mul=scalar, pow=none, pow_base=none | (-1/4 * cos((2 * x))) | — |
| ✅ certified | form=product, funcs=cos, fn_arg=var, mul=scalar, pow=none, pow_base=none | (-1 * cos(x)) | — |
| ⛔ withheld | form=product, funcs=erf,sqrt, fn_arg=other, mul=general, pow=none, pow_base=none | (1/2 * erf(x) * sqrt(pi)) | collect_mul_factors, diff_primitive_registry, diff_sqrt, mul_zero, product_rule |
| ⛔ withheld | form=product, funcs=exp,log, fn_arg=other, mul=general, pow=none, pow_base=none | (C1 * exp(log(x))) | diff_exp, product_rule |
| ✅ certified | form=product, funcs=exp,log, fn_arg=var, mul=general, pow=none, pow_base=none | (exp(x) * log(x)) | — |
| ✅ certified | form=product, funcs=exp,sin, fn_arg=var, mul=general, pow=none, pow_base=none | (exp(x) * sin(x)) | — |
| ✅ certified | form=product, funcs=exp,sinh, fn_arg=var, mul=general, pow=none, pow_base=none | (exp(x) * sinh(x)) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=other, mul=general, pow=nat, pow_base=var | (C1 * exp((1/2 * x^2))) | product_rule |
| ⛔ withheld | form=product, funcs=exp, fn_arg=other, mul=general, pow=none, pow_base=none | (C1 * exp((-1 * x))), (C1 * exp((3 * x))) | product_rule |
| ⛔ withheld | form=product, funcs=exp, fn_arg=pow, mul=scalar, pow=nat, pow_base=var | (1/2 * exp(x^2)) | product_rule |
| ✅ certified | form=product, funcs=exp, fn_arg=var, mul=general, pow=nat, pow_base=var | (exp(x) * x^2) | — |
| ✅ certified | form=product, funcs=exp, fn_arg=var, mul=general, pow=none, pow_base=none | ((-1 + x) * exp(x)), (C1 * exp(x)) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=other, mul=scalar, pow=nat, pow_base=var | (1/2 * log((-1 + x^2))), (1/2 * log((1 + x^2))) | diff_log, product_rule |
| ✅ certified | form=product, funcs=log, fn_arg=var, mul=general, pow=nat, pow_base=var | (log(x) * x^2), (log(x) * x^3) | — |
| ✅ certified | form=product, funcs=log, fn_arg=var, mul=general, pow=none, pow_base=none | (log(x) * x) | — |
| ⛔ withheld | form=product, funcs=sin, fn_arg=var, mul=general, pow=neg_one, pow_base=var | (sin(x) * x^-1) | product_rule |
| ✅ certified | form=product, funcs=sqrt, fn_arg=var, mul=general, pow=nat, pow_base=var | (sqrt(x) * x^2) | — |
| ✅ certified | form=product, funcs=sqrt, fn_arg=var, mul=general, pow=none, pow_base=none | (sqrt(x) * x) | — |
| ⛔ withheld | form=sum, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=expr | (3 + y^2) | power_rule, sum_rule |
| ✅ certified | form=sum, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var | (C1 + x^2) | — |
| ✅ certified | form=sum, funcs=-, fn_arg=none, mul=scalar, pow=nat, pow_base=var | ((-1 * 2 * x^2) + (-1 * 7) + (3 * x^3) + (5 * x)), ((2 * x) + x^3) | — |
| ⛔ withheld | form=sum, funcs=asin,sqrt, fn_arg=other, mul=general, pow=nat, pow_base=var | ((1/2 * sqrt(((-1 * x^2) + 4)) * x) + (2 * asin((1/2 * x)))) | diff_primitive_registry, diff_sqrt, product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=cos,sin, fn_arg=other, mul=general, pow=none, pow_base=none | ((-2 * C1 * sin((2 * x))) + (2 * C2 * cos((2 * x)))), ((C1 * cos((2 * x))) + (C2 * sin((2 * x)))) | product_rule, sum_rule |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=var, mul=general, pow=nat, pow_base=var | ((-2 * sin(x)) + (2 * cos(x) * x) + (sin(x) * x^2)) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=var, mul=general, pow=none, pow_base=none | ((-1 * C1 * sin(x)) + (C2 * cos(x))), ((-1 * cos(x) * x) + sin(x)), ((C1 * cos(x)) + (C2 * sin(x))) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=var, mul=none, pow=none, pow_base=none | (cos(x) + sin(x)) | — |
| ✅ certified | form=sum, funcs=cosh,sinh, fn_arg=var, mul=none, pow=none, pow_base=none | (cosh(x) + sinh(x)) | — |
| ⛔ withheld | form=sum, funcs=exp, fn_arg=other, mul=general, pow=none, pow_base=none | ((-1 * C1 * exp((-1 * x))) + (-1 * C2 * exp((-1 * x)) * x) + (C2 * exp((-1 * x)))), ((-1 * C1 * exp((-1 * x))) + (-2 * C2 * exp((-2 * x)))), ((-1 * C2 * exp((-1 * x))) + (C1 * exp(x))) | product_rule, sum_rule |
| ✅ certified | form=sum, funcs=exp, fn_arg=var, mul=general, pow=none, pow_base=none | ((C1 * exp(x)) + (C2 * exp(x) * x) + (C2 * exp(x))), ((C1 * exp(x)) + (C2 * exp(x) * x)), ((C1 * exp(x)) + C2) | — |
| ⛔ withheld | form=sum, funcs=log, fn_arg=other, mul=scalar, pow=nat, pow_base=var | ((-1 * log((-2 + x))) + (1/2 * log(((-4 * x) + 3 + x^2)))) | diff_log, product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=log, fn_arg=other, mul=scalar, pow=neg_one, pow_base=expr | (((-1 + x)^-1 * -1/2) + (-1/4 * log((-1 + x))) + (1/4 * log((1 + x)))) | diff_log, power_rule, product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=log, fn_arg=other, mul=scalar, pow=none, pow_base=none | ((-1 * log((-1 + x))) + log((-2 + x))), ((-1/2 * log((-3 + x))) + (-1/6 * log((-1 + x))) + (1/2 * log((-2 + x))) + (1/6 * log((-4 + x)))) | diff_log, product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=log, fn_arg=var, mul=general, pow=nat, pow_base=expr | (((log(x))^2 * x) + (-2 * log(x) * x) + (2 * x)) | collect_mul_factors, power_rule, product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=log, fn_arg=var, mul=general, pow=nat, pow_base=var | ((-1/4 * x^2) + (1/2 * log(x) * x^2)) | collect_mul_factors |
| ✅ certified | form=sum, funcs=log, fn_arg=var, mul=general, pow=none, pow_base=none | ((-1 * x) + (log(x) * x)) | — |
| ✅ certified | form=sum, funcs=log, fn_arg=var, mul=none, pow=none, pow_base=none | (log(x) + x) | — |
| ⛔ withheld | form=sum, funcs=sqrt, fn_arg=other, mul=general, pow=neg_one, pow_base=var | ((-1 * sqrt((1 + x^2)) * x^-1) + 1) | collect_mul_factors, diff_sqrt, mul_zero, product_rule, sum_rule |
integrate
50 shape classes — 25 certified, 25 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=apply, funcs=cos, fn_arg=other, mul=scalar, pow=none, pow_base=none, definite=no | cos((2 * x)) | — |
| ✅ certified | form=apply, funcs=cos, fn_arg=other, mul=scalar, pow=none, pow_base=none, definite=yes | cos((2 * x)) | — |
| ✅ certified | form=apply, funcs=cos, fn_arg=var, mul=none, pow=none, pow_base=none, definite=no | cos(x) | — |
| ✅ certified | form=apply, funcs=cos, fn_arg=var, mul=none, pow=none, pow_base=none, definite=yes | cos(x) | — |
| ⛔ withheld | form=apply, funcs=exp, fn_arg=other, mul=scalar, pow=nat, pow_base=var, definite=no | exp((-1 * x^2)) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=var, mul=none, pow=none, pow_base=none, definite=no | exp(x) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=var, mul=none, pow=none, pow_base=none, definite=yes | exp(x) | — |
| ✅ certified | form=apply, funcs=log, fn_arg=var, mul=none, pow=none, pow_base=none, definite=no | log(x) | — |
| ✅ certified | form=apply, funcs=log, fn_arg=var, mul=none, pow=none, pow_base=none, definite=yes | log(x) | — |
| ✅ certified | form=apply, funcs=sin, fn_arg=var, mul=none, pow=none, pow_base=none, definite=no | sin(x) | — |
| ✅ certified | form=apply, funcs=sin, fn_arg=var, mul=none, pow=none, pow_base=none, definite=yes | sin(x) | — |
| ⛔ withheld | form=apply, funcs=sqrt, fn_arg=other, mul=scalar, pow=nat, pow_base=var, definite=no | sqrt(((-1 * x^2) + 4)) | — |
| ⛔ withheld | form=apply, funcs=sqrt, fn_arg=var, mul=none, pow=none, pow_base=none, definite=yes | sqrt(x) | — |
| ⛔ withheld | form=apply, funcs=tan, fn_arg=var, mul=none, pow=none, pow_base=none, definite=no | tan(x) | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=frac, pow_base=var, definite=no | x^(1/2) | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var, definite=no | x^2, x^3, x^4 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var, definite=yes | x^2, x^3, x^4 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=neg, pow_base=var, definite=no | x^-2 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=neg_one, pow_base=var, definite=no | x^-1 | — |
| ⛔ withheld | form=power, funcs=log, fn_arg=var, mul=none, pow=nat, pow_base=expr, definite=no | (log(x))^2 | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=expr, definite=no | ((((-1 * 1) + x) * ((-1 * 2) + x) * ((-1 * 3) + x) * ((-1 * 4) + x))^-1 * 1), ((((-1 * 1) + x) * ((-1 * 2) + x) * ((-1 * 3) + x))^-1 * 1), ((((-1 * 1) + x) * ((-1 * 2) + x))^-1 * 1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=one_plus_sq, definite=no | ((1 + x^2)^-1 * x) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=one_plus_sq, definite=yes | ((1 + x^2)^-1 * x) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=nat, pow_base=var, definite=yes | (1/2 * x^2) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=expr, definite=no | ((((-1 * 1) + x)^2)^-1 * 1), ((4 + x^2)^-1 * 1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=expr, definite=yes | ((1 + x)^-1 * 1), ((4 + x^2)^-1 * 1), ((x^2)^-1 * 1) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=one_plus_sq, definite=no | ((1 + x^2)^-1 * 1) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=one_plus_sq, definite=yes | ((1 + x^2)^-1 * 1) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=var, definite=no | (1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=var, definite=yes | (1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=cos,sin, fn_arg=var, mul=general, pow=none, pow_base=none, definite=no | (cos(x) * sin(x)) | — |
| ✅ certified | form=product, funcs=cos, fn_arg=var, mul=general, pow=nat, pow_base=var, definite=no | (cos(x) * x^2) | — |
| ⛔ withheld | form=product, funcs=cos, fn_arg=var, mul=scalar, pow=neg_one, pow_base=expr, definite=no | (((cos(x))^2)^-1 * 1) | — |
| ✅ certified | form=product, funcs=cos, fn_arg=var, mul=scalar, pow=none, pow_base=none, definite=yes | (3 * cos(x)) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=pow, mul=general, pow=nat, pow_base=var, definite=no | (exp(x^2) * x) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=nat, pow_base=var, definite=yes | (exp(x) * x^2) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=neg_one, pow_base=var, definite=no | (exp(x) * x^-1) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=none, pow_base=none, definite=no | (exp(x) * x) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=none, pow_base=none, definite=yes | (exp(x) * x) | — |
| ✅ certified | form=product, funcs=exp, fn_arg=var, mul=scalar, pow=none, pow_base=none, definite=yes | (-1 * exp(x)) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=var, mul=general, pow=none, pow_base=none, definite=no | (log(x) * x) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=var, mul=general, pow=none, pow_base=none, definite=yes | (log(x) * x) | — |
| ⛔ withheld | form=product, funcs=sin, fn_arg=var, mul=general, pow=neg_one, pow_base=var, definite=no | (sin(x) * x^-1) | — |
| ✅ certified | form=product, funcs=sin, fn_arg=var, mul=general, pow=none, pow_base=none, definite=no | (sin(x) * x) | — |
| ⛔ withheld | form=product, funcs=sqrt, fn_arg=other, mul=general, pow=neg_one, pow_base=expr, definite=no | ((sqrt((1 + x^2)) * x^2)^-1 * 1), ((sqrt((1 + x^2)))^-1 * x) | — |
| ⛔ withheld | form=product, funcs=sqrt, fn_arg=other, mul=scalar, pow=neg_one, pow_base=expr, definite=no | ((sqrt(((-1 * 1) + x^2)))^-1 * 1), ((sqrt(((-1 * x^2) + 1)))^-1 * 1) | — |
| ⛔ withheld | form=product, funcs=sqrt, fn_arg=other, mul=scalar, pow=neg_one, pow_base=expr, definite=yes | ((sqrt(((-1 * x^2) + 1)))^-1 * 1) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=var, mul=none, pow=none, pow_base=none, definite=yes | (cos(x) + sin(x)) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=var, mul=scalar, pow=nat, pow_base=var, definite=yes | ((3 * cos(x)) + sin(x) + x^2) | — |
| ✅ certified | form=sum, funcs=exp,log, fn_arg=var, mul=general, pow=neg_one, pow_base=var, definite=no | ((exp(x) * log(x)) + (exp(x) * x^-1)) | — |
limit
26 shape classes — 9 certified, 17 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=apply, funcs=exp, fn_arg=other, mul=scalar, pow=none, pow_base=none, point=atTop | exp((-1 * x)) | — |
| ✅ certified | form=apply, funcs=exp, fn_arg=var, mul=none, pow=none, pow_base=none, point=atTop | exp(x) | — |
| ✅ certified | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none, point=atTop | x | — |
| ⛔ withheld | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none, point=zero | 5 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var, point=atTop | x^2 | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=sym, pow_base=var, point=zero | x^x | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=scalar, pow=sym, pow_base=expr, point=atTop | ((1 * x^-1) + 1)^x, ((2 * x^-1) + 1)^x | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=scalar, pow=sym, pow_base=expr, point=zero | (1 + x)^(1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=expr, point=atTop | (((2 * x) + 1) * (3 + x^2)^-1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=expr, point=finite | (((-1 * 1) + x)^-1 * ((-1 * 1) + x^2)), (((-1 * 2) + x)^-1 * ((-1 * 4) + x^2)), (((3 * x) + 2 + x^2) * (1 + x)^-1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=one_plus_sq, point=atTop | (((2 * x) + (3 * x^2)) * (1 + x^2)^-1), ((1 + x^2)^-1 * x^3) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=var, point=atTop | (1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one, pow_base=var, point=zero | (1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=cos, fn_arg=var, mul=general, pow=neg_one, pow_base=expr, point=zero | (((-1 * cos(x)) + 1) * (x^2)^-1) | — |
| ✅ certified | form=product, funcs=exp, fn_arg=other, mul=general, pow=nat, pow_base=var, point=atTop | (exp((-1 * x)) * x^2), (exp((-1 * x)) * x^3) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=other, mul=general, pow=neg_one, pow_base=var, point=zero | (((-1 * 1) + exp((2 * x))) * x^-1) | — |
| ✅ certified | form=product, funcs=exp, fn_arg=other, mul=general, pow=none, pow_base=none, point=atTop | (exp((-1 * x)) * x) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=neg_one, pow_base=expr, point=zero | (((-1 * 1) + (-1 * x) + exp(x)) * (x^2)^-1) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=neg_one, pow_base=var, point=atTop | (exp(x) * x^-1) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=neg_one, pow_base=var, point=zero | (((-1 * 1) + exp(x)) * x^-1) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=other, mul=general, pow=neg_one, pow_base=var, point=zero | (log((1 + x)) * x^-1) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=var, mul=general, pow=neg_one, pow_base=expr, point=finite | (((-1 * 1) + x)^-1 * log(x)) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=var, mul=general, pow=neg_one, pow_base=var, point=atTop | (log(x) * x^-1) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=var, mul=general, pow=none, pow_base=none, point=zero | (log(x) * x) | — |
| ✅ certified | form=product, funcs=sin, fn_arg=var, mul=general, pow=neg_one, pow_base=var, point=zero | (sin(x) * x^-1) | — |
| ⛔ withheld | form=product, funcs=sqrt, fn_arg=other, mul=general, pow=neg_one, pow_base=var, point=zero | (((-1 * 1) + sqrt((1 + x))) * x^-1) | — |
product_definite
1 shape classes — 1 certified.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none, definite=yes | k | — |
simplify
18 shape classes — 7 certified, 2 conditional, 9 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | form=apply, funcs=exp,log, fn_arg=other, mul=none, pow=none | exp(log(x)), log(exp(x)) | — |
| ⛔ withheld | form=apply, funcs=exp, fn_arg=other, mul=none, pow=none | exp((x + y)) | — |
| ⛔ withheld | form=apply, funcs=log, fn_arg=other, mul=general, pow=none | log((x * y)) | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=frac | (x^(1/2))^2 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=nat | (x^2)^3, x^0, x^1 | — |
| 🟡 conditional | form=power, funcs=-, fn_arg=none, mul=none, pow=neg | (x^3)^-2, k^-2, k^-3 | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=neg_one | (x^-1)^-1 | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=frac | (x^(1/3) * x^(2/3)) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=general, pow=nat | (x^2 * x^3) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=general, pow=neg | (x^-2 * x^2), (x^-2 * x^5) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one | (x^-1 * x^2) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg_one | ((k^2)^-1 * 3), ((x^3)^-1 * 1) | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=scalar, pow=none | (0 * x), (1 * x), (3 * 4) | — |
| ⛔ withheld | form=product, funcs=gamma, fn_arg=other, mul=general, pow=none | (gamma((1 + k)) * k) | — |
| ⛔ withheld | form=product, funcs=log, fn_arg=other, mul=scalar, pow=none | (2 * log(x)) | — |
| 🟡 conditional | form=sum, funcs=-, fn_arg=none, mul=none, pow=none | (0 + x), (2 + 3), (2 + x) | — |
| ⛔ withheld | form=sum, funcs=-, fn_arg=none, mul=scalar, pow=none | ((2 * k) + 1) | — |
| ⛔ withheld | form=sum, funcs=log, fn_arg=other, mul=scalar, pow=none | ((-1 * log(y)) + log(x)) | — |
simplify_log_exp
6 shape classes — 6 certified.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=apply, funcs=exp,log, fn_arg=other, mul=none, pow=none | exp(log(x)), log(exp(x)) | — |
| ✅ certified | form=apply, funcs=log, fn_arg=other, mul=general, pow=neg_one | log((x * y^-1)) | — |
| ✅ certified | form=apply, funcs=log, fn_arg=other, mul=none, pow=nat | log(x^2) | — |
| ✅ certified | form=product, funcs=exp, fn_arg=other, mul=general, pow=none | (exp(x) * exp(y)) | — |
| ✅ certified | form=sum, funcs=exp,log, fn_arg=other, mul=none, pow=none | (exp(log(y)) + log(exp(x))) | — |
| ✅ certified | form=sum, funcs=log, fn_arg=other, mul=none, pow=none | (log(x) + log(y)) | — |
simplify_trig
21 shape classes — 14 certified, 7 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=apply, funcs=cos, fn_arg=other, mul=scalar, pow=none | cos((-1 * x)) | — |
| ✅ certified | form=apply, funcs=sin, fn_arg=other, mul=scalar, pow=none | sin((-1 * x)) | — |
| ⛔ withheld | form=apply, funcs=sinh, fn_arg=other, mul=scalar, pow=none | sinh((-1 * x)) | — |
| ✅ certified | form=apply, funcs=tan, fn_arg=other, mul=none, pow=none | tan(x) | — |
| ✅ certified | form=product, funcs=cos,sin, fn_arg=other, mul=general, pow=none | (2 * cos(x) * sin(x)) | — |
| ⛔ withheld | form=product, funcs=cos,tan, fn_arg=other, mul=general, pow=none | (cos(x) * tan(x)) | collect_mul_factors |
| ✅ certified | form=product, funcs=cos, fn_arg=other, mul=general, pow=neg_one | (((-1 * cos((2 * x))) + 1) * 2^-1) | — |
| ⛔ withheld | form=product, funcs=cosh,sinh, fn_arg=other, mul=general, pow=neg_one | ((cosh(x))^-1 * sinh(x)) | — |
| ⛔ withheld | form=product, funcs=cosh,sinh, fn_arg=other, mul=general, pow=none | (2 * cosh(x) * sinh(x)) | — |
| ⛔ withheld | form=product, funcs=sin,tan, fn_arg=other, mul=general, pow=neg_one | ((tan(x))^-1 * sin(x)) | collect_mul_factors, pow_of_product_cancel |
| ✅ certified | form=product, funcs=sin, fn_arg=other, mul=general, pow=neg_one | ((sin(x))^-1 * 1 * sin(x)) | — |
| ✅ certified | form=sum, funcs=cos,sin,tan, fn_arg=other, mul=general, pow=neg_one | (((cos(x))^-1 * -1 * sin(x)) + tan(x)), (((cos(x))^-1 * sin(x)) + (-1 * tan(x))) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=other, mul=general, pow=none | ((cos(x) * cos(x)) + (sin(x) * sin(x))) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=other, mul=none, pow=nat | ((cos(x))^2 + (sin(x))^2) | — |
| ⛔ withheld | form=sum, funcs=cos,sin, fn_arg=other, mul=scalar, pow=nat | (((((sin(x))^2 * -1 * 2) + 1) * -1) + cos((2 * x))) | zero_sum |
| ✅ certified | form=sum, funcs=cos, fn_arg=other, mul=scalar, pow=nat | (((cos(x))^2 * 2) + (-1 * 1)) | — |
| ✅ certified | form=sum, funcs=cosh,sinh, fn_arg=other, mul=scalar, pow=nat | (((sinh(x))^2 * -1) + (cosh(x))^2) | — |
| ✅ certified | form=sum, funcs=cosh, fn_arg=other, mul=scalar, pow=nat | (((cosh(x))^2 * 2) + (-1 * 1)) | — |
| ✅ certified | form=sum, funcs=sin, fn_arg=other, mul=scalar, pow=nat | (((sin(x))^2 * -1 * 2) + 1) | — |
| ✅ certified | form=sum, funcs=tan, fn_arg=other, mul=none, pow=nat | ((tan(x))^2 + 1) | — |
| ⛔ withheld | form=sum, funcs=tanh, fn_arg=other, mul=scalar, pow=nat | (((tanh(x))^2 * -1) + 1) | — |
sum_definite
9 shape classes — 5 certified, 4 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none, definite=yes | 5, k | — |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var, definite=yes | k^2, k^3 | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=neg, pow_base=var, definite=yes | k^-2, k^-3, k^-4 | basel_zeta_even, rational_series_partial_fractions |
| ✅ certified | form=power, funcs=-, fn_arg=none, mul=none, pow=sym, pow_base=int, definite=yes | 2^k | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=sym, pow_base=recip, definite=yes | (1/2)^k | — |
| ✅ certified | form=product, funcs=-, fn_arg=none, mul=general, pow=neg_one, pow_base=expr, definite=yes | (((1 + k) * k)^-1 * 1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg, pow_base=var, definite=yes | (3 * k^-2) | basel_zeta_even |
| ⛔ withheld | form=product, funcs=gamma, fn_arg=other, mul=general, pow=none, pow_base=none, definite=yes | (gamma((1 + k)) * k) | — |
| ✅ certified | form=sum, funcs=-, fn_arg=none, mul=scalar, pow=none, pow_base=none, definite=yes | ((2 * k) + 1) | — |
sum_indefinite
1 shape classes — 1 certified.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none | k | — |
Querying it
import alkahest as ak
p = ak.ExprPool()
x = p.symbol("x")
# Will this route give me something a referee can check?
answer = ak.certifiable("diff", ak.log(ak.sin(x)), x)
bool(answer) # False
# Plan across candidate routes without computing any of them.
ak.certifiable("diff", ak.sin(x), x, mode="ledger")
# Fail loudly instead of degrading silently.
with ak.context(require_certificate=True):
ak.diff(ak.log(ak.sin(x)), x) # raises E-CERT-001