Lean certificates

Alkahest can emit Lean 4 source for derivations. Generated source becomes a machine-checked proof only after it typechecks with the pinned Lean/Mathlib toolchain and without admitted placeholders.

Three levels of evidence

Derivation logs — always on, always cheap. Records every rewrite rule applied, with rule name and arguments. Human-readable; machine-parseable; forms the basis for Lean export.

Lean certificate export — for computations expressible as sequences of rewrites tagged with Lean theorem names. The library emits a .lean file containing a proof term. Emission makes a certificate available; it does not by itself mean Lean has checked the source.

In the agent contract, certificate_available has this same meaning. Only a corpus artifact compiled by pinned Lean/Mathlib without admissions can be described as lean_checked — and because that compilation happens out of process, in CI, no DerivedResult ever reports lean_checked as its status. It is therefore not listed in capabilities()["verification"]["statuses"], which enumerates only the statuses the library can actually emit.

Algorithmic certificates — planned evidence for operations where rewrite sequences do not work. Do not treat a derivation log as an independently verified witness.

Theorem mapping

Every primitive in the registry is tagged with a Lean 4 / Mathlib theorem name:

The full mapping lives in alkahest-core/src/lean/.

Exporting a certificate

from alkahest import diff, sin

pool = ExprPool()
x = pool.symbol("x", "real")

dr = diff(sin(x**2), x)

# The certificate is in dr.certificate when Lean export is enabled
if dr.certificate:
    with open("proof.lean", "w") as f:
        f.write(dr.certificate)

The emitted .lean file imports Mathlib and contains a proof term that Lean can verify:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

-- Alkahest certificate: d/dx sin(x²) = 2*x*cos(x²)
theorem alkahest_diff_sin_sq (x : ℝ) :
    HasDerivAt (fun x => Real.sin (x ^ 2)) (2 * x * Real.cos (x ^ 2)) x := by
  have h1 : HasDerivAt (fun x => x ^ 2) (2 * x) x := ...
  exact (Real.hasDerivAt_sin _).comp x h1

Strict Lean CI

The CI pipeline (.github/workflows/lean.yml) generates a deliberately small, strict corpus of basic arithmetic rewrites and d/dx x³. Every corpus entry must have the expected non-empty derivation log, must contain no sorry, admit, or axiom, and must typecheck with warnings treated as errors. The pinned Lean 4.9 compiler does not provide a --no-sorries command-line flag, so the source admission check is explicit in both the generator and CI.

1. Generates proof files via tests/lean_corpus.py
2. Compiles them with the pinned Lean/Mathlib toolchain (with Mathlib cached)
3. Fails the build if a proof contains an admission or does not typecheck

Knowing where the line is, before you compute

The boundary above is not something to discover by running an operation and finding .certificate is None. It is tabulated in Certificate coverage — a table generated by running a corpus and recording what actually emitted, checked into the repo, and pinned by a CI drift check. Three ways to use it:

import alkahest as ak

p = ak.ExprPool()
x = p.symbol("x")

# 1. Ask before you commit to a route. Truthy iff a certificate is produced;
#    carries the reason when it is not.
answer = ak.certifiable("integrate", ak.log(x), x)
bool(answer)        # False
answer.reason       # 'class_withheld'

# `mode="ledger"` answers from the table alone, running nothing at all —
# for scoring many candidate routes. The default `mode="verify"` never says
# True without the certificate in hand, and hands the computed result back on
# `answer.result` so the check costs nothing extra.

# 2. Read the whole boundary.
[r["shape"] for r in ak.certificate_coverage("diff") if r["verdict"] == "certified"]

# 3. Refuse to degrade silently.
with ak.context(require_certificate=True):
    ak.integrate(ak.log(x), x)   # raises CertificateUnavailableError (E-CERT-001)

capabilities()["verification"]["coverage"] summarises the same ledger, and each primitive’s lean_theorem bit is read from it — so the agent contract and the coverage table cannot disagree.

Coverage

The strict CI corpus currently covers:

• Basic arithmetic rewrites (add_zero, mul_one, mul_zero, constant folding, and pow_one)
• The polynomial differentiation fast path for d/dx x³
• Indefinite integrals of sin, cos, exp, and xⁿ, certified via the FTC derivative relation deriv (fun x => F) x = f
• Definite integrals ∫ x in a..b, f x = F b - F a of the same base family (sin, cos, exp, xⁿ), plus finite sums and numeric-literal constant multiples of those terms (∫ (sin x + cos x), ∫ 3·cos x, ∫ -exp x, ∫ (x² + sin x + 3·cos x), …), certified via Mathlib’s interval-FTC lemma (intervalIntegral.integral_eq_sub_of_hasDerivAt) composed with HasDerivAt.add/.const_mul/.mul_const and the matching IntervalIntegrable combinators. A symbolic (non-literal) coefficient, or any addend outside the base family, withholds the whole certificate.

Other exports are generated source, not CI-qualified Lean proofs. In particular, non-polynomial differentiation, conditional logarithm/power rewrites, integration, limits, and unsupported expression forms can require side conditions or currently use a placeholder tactic. They must remain unverified until their proof encoding and strict corpus coverage are added.

Planned algorithmic certificates include:

• Polynomial factoring
• Polynomial GCD

Side conditions in proofs

Side conditions (domain constraints and branch-cut restrictions) are recorded in the derivation log. They are not yet translated into Lean hypotheses by the exporter, so conditional rewrites are excluded from the strict corpus.