Trust and verification
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: 334 observations over 212 shape classes — 121 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, plus the outermost function, head, for a variable-free operation on a function application).
| 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
78 shape classes — 51 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=piecewise, funcs=-, fn_arg=none, mul=scalar, pow=nat, pow_base=var, cond=var_cmp |
<piecewise> |
— |
| ✅ certified | form=piecewise, funcs=sin, fn_arg=var, mul=none, pow=nat, pow_base=var, cond=var_cmp |
<piecewise> |
— |
| ✅ 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
19 shape classes — 8 certified, 2 conditional, 9 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | form=apply, head=exp, funcs=exp,log, fn_arg=other, mul=none, pow=none |
exp(log(x)) |
exp_of_log_nonzero |
| ⛔ withheld | form=apply, head=exp, funcs=exp, fn_arg=other, mul=none, pow=none |
exp((x + y)) |
— |
| ✅ certified | form=apply, head=log, funcs=exp,log, fn_arg=other, mul=none, pow=none |
log(exp(x)) |
— |
| ⛔ withheld | form=apply, head=log, 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
7 shape classes — 7 certified.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ✅ certified | form=apply, head=exp, funcs=exp,log, fn_arg=other, mul=none, pow=none |
exp(log(x)) |
— |
| ✅ certified | form=apply, head=log, funcs=exp,log, fn_arg=other, mul=none, pow=none |
log(exp(x)) |
— |
| ✅ certified | form=apply, head=log, funcs=log, fn_arg=other, mul=general, pow=neg_one |
log((x * y^-1)) |
— |
| ✅ certified | form=apply, head=log, 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, head=cos, funcs=cos, fn_arg=other, mul=scalar, pow=none |
cos((-1 * x)) |
— |
| ✅ certified | form=apply, head=sin, funcs=sin, fn_arg=other, mul=scalar, pow=none |
sin((-1 * x)) |
— |
| ⛔ withheld | form=apply, head=sinh, funcs=sinh, fn_arg=other, mul=scalar, pow=none |
sinh((-1 * x)) |
— |
| ✅ certified | form=apply, head=tan, 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
Python
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):
try:
ak.diff(ak.log(ak.sin(x)), x)
except ak.CertificateUnavailableError as e:
print(e.code) # E-CERT-001