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

The corpus is a lower bound on correctness, not a proof of it. A shape the corpus never emits is never typechecked, and the emitter is broader than the corpus: several arms shipped emitting .lean files that Lean rejects simply because nothing generated them. Two lessons are baked into the corpus now.

Assert the goal, not the theorem’s name. A test that checks only that a Mathlib lemma is mentioned somewhere in the file passes just as happily when the goal above it says something else. Corpus entries that depend on a particular printed form pin that form (_require_goal), and the tactic assertion for an instantiated lemma includes the argument (tendsto_pow_mul_exp_neg_atTop_nhds_zero 2, not the bare name).

Commutative order is not stable. Children of Add/Mul are canonicalised by raw ExprId, so which addend or factor prints first depends on what else the pool interned — the same call certified in a fresh pool and emitted a non-compiling file in a warm one. Where a certificate’s tactic is sensitive to that order, the corpus builds both orders deliberately (a fresh ExprPool per case, with the flipping term interned first).

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("diff", ak.log(ak.sin(x)), x)
bool(answer)        # False

# `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.diff(ak.log(ak.sin(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³
• Chain-rule differentiation of f(g x) for f ∈ {sin, cos, exp} and inner g a power xⁿ (n ≥ 2), a linear form c·x / x+c / a+bx (including interned -x as x * -1), or a pointwise sin/cos/exp of the variable (sin(cos x), exp(-x), cos(2x), exp(-x²))
• Indefinite integrals of sin, cos, exp, log, and xⁿ, certified via the FTC derivative relation deriv (fun x => F) x = f. ∫ log x reuses the product/sum certificate for d/dx (x log x − x). Definite ∫_a^b log x certifies when both endpoints are strictly positive.
• Products and sums that mix the everywhere-differentiable fragment with pointwise log(x) / sqrt(x) (x log x, exp x · log x, log x + x, x sqrt x), with an explicit (hx : 0 < x) binder. Composites (log(x²), log(sqrt(x²−1)+x)) stay withheld. ∫ x log x stays withheld: d/dx of its antiderivative has an n-ary inverse cancellation (x² · x⁻¹ · ½) that the two-factor field_simp encoding does not close.
• 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. Pointwise ∫_a^b log x is a separate arm: it needs 0 < a and 0 < b (intervalIntegrable_log requires 0 ∉ uIcc a b) and proves F b − F a for F = x log x − x. ∫_0^1 log and negative endpoints stay withheld.
• Gosper finite sums ∑_{k=a}^{b} F(k) = G(b+1) − G(a) for polynomial, rational-telescope, and geometric terms, certified as a Finset.sum identity via sum_range_sub / sum_Ico_eq_sum_range — never as the false rewrite F = G. Infinite Basel sums and gamma encodings stay withheld.
• The discrete product ∏_{k=1}^{n} k = n!, via Mathlib Finset.prod_Ico_id_eq_factorial (v4.9.0 has no prod_Icc_id).

Other exports are generated source, not CI-qualified Lean proofs. In particular, nested two-deep composites (sin(cos(x²))), log/tan/sqrt chain, conditional logarithm/power rewrites, integration outside the FTC fragment, 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.