Python API

Certificates API

Lean certificates

function

to_lean(arg)

#source

alkahest.to_lean(expr_or_result) -> str

Generate a Lean 4 proof certificate from a derivation.

Accepts:

An Expr — the default simplifier runs first, then the derivation log is certified. Equivalent to to_lean(simplify(expr)).
A DerivedResult returned by any operation — exactly its certificate: a rewrite log as one example per step, an integral via the FTC derivative relation, a limit via Filter.Tendsto, a Gosper sum via a Finset telescope, a resultant as its Sylvester determinant (up to 7×7), the derivative of a Piecewise branch by branch on each branch's open region.
Any object with its own to_lean() method (e.g. a PositivityCertificate, or a ZeilbergerCertificate, whose certificate is the telescoping identity).

Every free variable of the statement is universally bound by an explicit (x : ℝ) binder, and the statement is the computed result itself — never an algorithm's input restated as equal to its output.

Returns a string containing the complete .lean source file. It never returns an empty string: when no sound certificate exists (the shape is outside the certifiable fragment, nothing was derived, or the object has no Lean encoding at all), it raises CertificateUnavailableError (E-CERT-001).

Example:

Python

result = alkahest.simplify_trig(sin(x)**2 + cos(x)**2)
print(alkahest.to_lean(result))  # certifies via trig identities

Certifiability

function

certifiable(op, *args, mode: str='verify', **kwargs) → Certifiability

#source

Will running op on these arguments produce a Lean certificate?

Parameters

opstr or callable

Operation name ("integrate") or the function itself (alkahest.integrate). See OPERATIONS for the tracked set.

*args, **kwargs

The arguments you would pass to op.

mode{"verify", "ledger"}

"verify" (default) is sound: it never answers True without a certificate in hand. It short-circuits to False for shape classes the ledger records as never certifying, and otherwise runs op and inspects the result — which it hands back on Certifiability.result, so the work is not wasted.

"ledger" runs nothing at all and answers from the checked-in coverage table. Use it for planning across many candidate routes where even one evaluation each is too much. Its True is an empirical claim about the shape class, validated against the corpus in CI, not a certificate in hand.

Returns

Certifiability: Truthy iff a certificate is (or would be) produced; carries the reason.

Examples

Python

>>> import alkahest as ak
>>> p = ak.ExprPool(); x = p.symbol("x")
>>> bool(ak.certifiable("diff", ak.sin(x), x))
True
>>> answer = ak.certifiable("diff", ak.log(ak.sin(x)), x)
>>> bool(answer)
False

Plan a route without computing anything:

Python

routes = [("integrate", f, x), ("diff", F, x)]
best = max(routes, key=lambda r: bool(ak.certifiable(*r, mode="ledger")))

class

class Certifiability(
    *,
    certifiable: bool,
    operation: str,
    shape: str,
    verdict: str,
    reason: str,
    detail: str,
    checked: bool=False,
    result: Any=None,
    error: Exception | None=None,
    evidence: dict[str, Any] | None=None
)

#source

The answer to "will this call yield a Lean certificate?".

Truthy exactly when a certificate is (or would be) produced, so it drops into if certifiable(...): — but it carries the reason, which is what a planning loop actually needs.

Attributes

certifiablebool: The verdict. bool(self) is the same value.
operationstr: The operation asked about.
shapestr: Shape-class key (see certificate_coverage()).
verdictstr: Ledger verdict for the shape class: "certified", "withheld", "conditional", "partial", or "unknown" (never observed).
reasonstr: Stable reason code. "emitted" / "withheld_no_derivation" / "withheld_uncertifiable_step" / "withheld_integration_shape" / "withheld_tendsto_shape" / "withheld_gosper_shape" / "withheld_product_shape" / "withheld_resultant_shape" come from actually running the operation; "class_certified" / "class_withheld" / "class_conditional" / "class_partial" / "unknown_shape" come from the ledger alone; "operation_failed" means the operation itself raised.
detailstr: One-sentence human explanation.
checkedbool: True when the operation was actually run, so the verdict is exact rather than predicted.
resultDerivedResult or None: The result computed while checking — returned so a caller that goes on to use it does not pay for the computation twice.
errorException or None: The exception raised by the operation, if any.
evidencedict or None: The ledger row backing this answer.

Methods

as_dict() → dict[str, Any]

#source

JSON-serialisable view (omits result, which is not serialisable).

function

require_certificate(result)

#source

Return result if it carries a Lean certificate; otherwise raise.

The per-call form of the ambient with alkahest.context(require_certificate=True) mode. Use it to turn a silent degradation — a result that quietly arrives without evidence — into a loud, coded failure at the point it happens.

Parameters

resultDerivedResult: The result to check. Returned unchanged when it certifies, so this wraps a call inline.

Returns

DerivedResult

Raises

CertificateUnavailableError: E-CERT-001, carrying the withholding reason and any blocking rewrite rules in its remediation text.

Examples

Python

>>> import alkahest as ak
>>> p = ak.ExprPool(); x = p.symbol("x")
>>> ak.require_certificate(ak.diff(ak.sin(x), x)).value
cos(x)

Ambient form, for a loop that must not produce uncertified claims:

Python

with ak.context(require_certificate=True):
    claim = ak.integrate(f, x)   # raises E-CERT-001 rather than
                                 # returning an uncertified result

function

certificate_coverage(operation: str | None=None) → list[dict[str, Any]]

#source

Return the generated per-operation certificate coverage table.

Each row describes one shape class:

Python

{
  "operation":    "integrate",
  "shape":        "integrate/form=apply/funcs=log/...",
  "features":     {"form": "apply", "funcs": "log", ...},
  "verdict":      "withheld",
  "observations": {"certified": 0, "withheld": 3, "no_derivation": 0},
  "examples":     ["log(x)", ...],
}

verdict is one of:

certified Every corpus observation of this shape emitted a certificate. certifiable() answers True here and nowhere else. withheld No observation emitted; the emitter cannot prove this shape today. conditional Emits when the operation actually rewrites something, but some observations had an empty derivation log (nothing to prove). Not predictable from the arguments alone, so certifiable() answers False with reason "class_conditional". partial Mixed certified and withheld observations — the shape class is too coarse to separate them. The generator reports these; a healthy tree has none.

Parameters

operationstr, optional: Restrict to one operation (e.g. "diff").

Returns

list of dict: Sorted by operation then shape.

Examples

Python

>>> import alkahest as ak
>>> withheld = [r for r in ak.certificate_coverage("integrate")
...             if r["verdict"] == "withheld"]

Certificates API

#Lean certificates

#Certifiability

Lean certificates

Certifiability