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).
Corpus: 240 observations over 156 shape classes — 66 certified, 2 conditional, 0 partial, 88 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
63 shape classes — 26 certified, 37 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | form=apply, funcs=asin, fn_arg=var, mul=none, pow=none, pow_base=none | asin(x) | diff_primitive_registry |
| ⛔ withheld | form=apply, funcs=atan, fn_arg=var, mul=none, pow=none, pow_base=none | atan(x) | diff_primitive_registry |
| ⛔ withheld | form=apply, funcs=atan2, fn_arg=other, mul=none, pow=none, pow_base=none | atan2(x, 1) | diff_primitive_registry |
| ⛔ withheld | form=apply, funcs=cos,sin, fn_arg=other, mul=none, pow=none, pow_base=none | sin(cos(x)) | diff_sin |
| ✅ 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) | — |
| ⛔ withheld | form=apply, funcs=cosh, fn_arg=var, mul=none, pow=none, pow_base=none | cosh(x) | diff_primitive_registry |
| ⛔ withheld | form=apply, funcs=exp, fn_arg=other, mul=scalar, pow=nat, pow_base=var | exp((-1 * x^2)) | diff_exp |
| ✅ 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) | — |
| ⛔ withheld | form=apply, funcs=sinh, fn_arg=var, mul=none, pow=none, pow_base=none | sinh(x) | diff_primitive_registry |
| ⛔ 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) | — |
| ⛔ withheld | form=apply, funcs=tanh, fn_arg=var, mul=none, pow=none, pow_base=none | tanh(x) | diff_primitive_registry |
| ✅ 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 | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=neg, pow_base=var | x^-2 | power_rule |
| ✅ 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, pow_base=expr | (sin(x))^-1 | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg, 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, pow_base=expr | ((-1 + x)^-1 * -1) | power_rule, product_rule |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg, pow_base=var | (-1 * x^-1) | power_rule, product_rule |
| ⛔ 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 |
| ⛔ 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, 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)) | — |
| ⛔ withheld | form=product, funcs=cos, fn_arg=other, mul=scalar, pow=none, pow_base=none | (-1/4 * cos((2 * x))) | diff_cos, product_rule |
| ✅ certified | form=product, funcs=cos, fn_arg=var, mul=scalar, pow=none, pow_base=none | (-1 * cos(x)) | — |
| ⛔ withheld | form=product, funcs=exp,log, fn_arg=other, mul=general, pow=neg, pow_base=expr | ((exp((-1 * log(x))))^-1 * C2) | diff_exp, power_rule, product_rule |
| ⛔ withheld | form=product, funcs=exp,log, fn_arg=var, mul=general, pow=none, pow_base=none | (exp(x) * log(x)) | product_rule |
| ✅ certified | form=product, funcs=exp,sin, fn_arg=var, mul=general, pow=none, pow_base=none | (exp(x) * sin(x)) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=other, mul=general, pow=neg, pow_base=expr | ((exp((-1 * x)))^-1 * C2), ((exp((-1/2 * x^2)))^-1 * C2), ((exp((-3 * x)))^-1 * C2) | collect_mul_factors, diff_exp, power_rule, 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) | — |
| ⛔ withheld | form=product, funcs=exp, fn_arg=var, mul=general, pow=neg, pow_base=expr | ((exp(x))^-1 * C2) | product_rule |
| ✅ 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 |
| ⛔ withheld | form=product, funcs=sin, fn_arg=var, mul=general, pow=neg, pow_base=var | (sin(x) * x^-1) | power_rule, product_rule |
| ⛔ withheld | form=product, funcs=sqrt, fn_arg=other, mul=scalar, pow=neg, pow_base=expr | (((sqrt((1 + x^2)) + x)^2 + -1)^-1 * -2) | diff_sqrt, power_rule, product_rule, sum_rule |
| ⛔ 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 | (((((2 * x^2) * -1) + (3 * x^3)) + (5 * x)) + (-1 * 7)) | — |
| ⛔ 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)))) * -1) + (4 * 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)))) | diff_cos, diff_sin, product_rule, sum_rule |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=var, mul=general, pow=nat, pow_base=var | ((((-2 * cos(x) * x) + (2 * sin(x))) * -1) + (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)) | — |
| ⛔ 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))) | diff_exp, 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, 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)) | 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)) | product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=log, fn_arg=var, mul=general, pow=none, pow_base=none | ((-1 * x) + (log(x) * x)) | product_rule, sum_rule |
| ⛔ withheld | form=sum, funcs=sqrt, fn_arg=other, mul=scalar, pow=neg, pow_base=expr | (((sqrt((1 + x^2)) + x) * 1/2) + ((sqrt((1 + x^2)) + x)^-1 * 1/2)) | diff_sqrt, power_rule, product_rule, sum_rule |
integrate
41 shape classes — 14 certified, 27 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | 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) | — |
| ✅ 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) | — |
| ⛔ withheld | form=apply, funcs=log, fn_arg=var, mul=none, pow=none, pow_base=none, definite=no | 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 | — |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=neg, pow_base=var, definite=no | x^-2 | — |
| ⛔ 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, 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, pow_base=expr, 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, pow_base=expr, definite=no | ((((-1 * 1) + x)^2)^-1 * 1), ((1 + x^2)^-1 * 1), ((4 + x^2)^-1 * 1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg, pow_base=expr, definite=yes | ((1 + x)^-1 * 1), ((1 + x^2)^-1 * 1), ((4 + x^2)^-1 * 1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg, pow_base=var, definite=no | (1 * x^-1) | — |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=scalar, pow=neg, 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)) | — |
| ⛔ withheld | 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, 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=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) | — |
| ✅ 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, 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, 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, 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)) | — |
| ⛔ withheld | form=sum, funcs=exp,log, fn_arg=var, mul=general, pow=neg, pow_base=var, definite=no | ((exp(x) * log(x)) + (exp(x) * x^-1)) | — |
simplify
16 shape classes — 5 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^-1)^-1, (x^3)^-2, k^-2 | — |
| ⛔ 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=scalar, pow=neg | ((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 | 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 — 15 certified, 6 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 * sin(x)) * cos(x)) | — |
| ✅ certified | form=product, funcs=cos,tan, fn_arg=other, mul=general, pow=none | (cos(x) * tan(x)) | — |
| ⛔ withheld | form=product, funcs=cos, fn_arg=other, mul=general, pow=neg | (((-1 * cos((2 * x))) + 1) * 2^-1) | — |
| ⛔ withheld | form=product, funcs=cosh,sinh, fn_arg=other, mul=general, pow=neg | ((cosh(x))^-1 * sinh(x)) | — |
| ✅ certified | form=product, funcs=cosh,sinh, fn_arg=other, mul=general, pow=none | ((2 * sinh(x)) * cosh(x)) | — |
| ✅ certified | form=product, funcs=sin,tan, fn_arg=other, mul=general, pow=neg | ((tan(x))^-1 * sin(x)) | — |
| ✅ certified | form=product, funcs=sin, fn_arg=other, mul=general, pow=neg | (((sin(x))^-1 * 1) * sin(x)) | — |
| ✅ certified | form=sum, funcs=cos,sin,tan, fn_arg=other, mul=general, pow=neg | ((((cos(x))^-1 * sin(x)) * -1) + 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) | — |
| ✅ certified | form=sum, funcs=cos,sin, fn_arg=other, mul=scalar, pow=nat | ((((((sin(x))^2 * 2) * -1) + 1) * -1) + cos((2 * x))) | — |
| ⛔ withheld | 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) | — |
| ⛔ withheld | 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 * 2) * -1) + 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
8 shape classes — 8 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none, definite=yes | 5, k | gosper_definite_telescope |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=nat, pow_base=var, definite=yes | k^2, k^3 | gosper_definite_telescope |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=neg, pow_base=var, definite=yes | k^-2, k^-4 | basel_zeta_even |
| ⛔ withheld | form=power, funcs=-, fn_arg=none, mul=none, pow=sym, pow_base=expr, definite=yes | (1/2)^k, 2^k | gosper_definite_telescope |
| ⛔ withheld | form=product, funcs=-, fn_arg=none, mul=general, pow=neg, pow_base=expr, definite=yes | (((1 + k) * k)^-1 * 1) | gosper_definite_telescope |
| ⛔ 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) | gosper_definite_telescope |
| ⛔ withheld | form=sum, funcs=-, fn_arg=none, mul=scalar, pow=none, pow_base=none, definite=yes | ((2 * k) + 1) | gosper_definite_telescope |
sum_indefinite
1 shape classes — 1 withheld.
| Verdict | Shape | Examples | Blocked by |
|---|---|---|---|
| ⛔ withheld | form=atom, funcs=-, fn_arg=none, mul=none, pow=none, pow_base=none | k | gosper_indefinite |
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("integrate", ak.log(x), x)
bool(answer) # False
answer.reason # 'class_withheld'
# 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.integrate(ak.log(x), x) # raises E-CERT-001