Skip to content

Python API · Submodule

alkahest.research

Session-level provenance for autoresearch loops — the Alkahest claim graph.

DerivedResult is a per-call object: it carries a value, a derivation log, an optional Lean certificate, and verification metadata for one computation. A research loop that runs for days produces thousands of them and has nowhere to put them, so its output degrades into a chat transcript — and transcripts do not survive context compaction.

This module supplies the missing session-level artifact: a directed acyclic graph of claims. Each Claim carries

a stable, content-addressed identifier derived from the normalised statement, the hypotheses, and the method — so the same claim derived twice, in different processes or on different days, gets the same ID and citing it across runs is meaningful;
the statement (an Expr, an equation, or free text);
the hypotheses it holds under, taken from Assumptions (hypotheses travel with the claim rather than living in an agent's context window, where they are dropped at the next compaction);
the derivation (DerivedResult.steps);
certificate text and verification status, copied verbatim;
provenance metadata (operation, arguments, Alkahest version, build features);
dependency edges to the claim IDs it was derived from.

The graph serialises to a versioned, deterministic, diffable JSON document (ClaimGraph.to_json()), renders to Markdown and LaTeX (ClaimGraph.to_markdown(), ClaimGraph.to_latex()), and can be re-verified against a newer library version (ClaimGraph.verify()).

Honesty invariant

The recording layer never upgrades a claim's status. A claim's status is whatever DerivedResult.verification["status"] said; claims created by ResearchSession.conjecture() are always "unverified", and there is no parameter to say otherwise. ClaimGraph.verify() may only lower confidence — a failed re-check marks a claim "refuted"; a successful re-check is recorded as an audit entry and does not promote anything.

Quick start

Python

>>> import alkahest as ak
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> with ak.research.session(title="Demo", pool=pool, capture=True) as s:
...     result = ak.integrate(x / (x**2 + pool.integer(1)), x)   # captured
>>> graph = s.graph
>>> len(graph) >= 1
True
>>> doc = graph.to_markdown()

class

class research.Claim

One recorded mathematical claim and everything needed to audit it.

Instances are immutable; ClaimGraph produces updated copies via dataclasses.replace() rather than mutating in place.

Attributes

idstr: Content-addressed identifier (see claim_id()).
statementstr: Normalised statement text.
kindstr: "expr" when the statement is an expression/equation, "text" for a prose claim or conjecture.
latexstr or None: LaTeX rendering of the statement, when it is an expression.
hypothesestuple of str: Predicates from the governing Assumptions.
methodstr: Operation that produced the claim, e.g. "integrate".
statusstr: Copied verbatim from DerivedResult.verification["status"], or "unverified" for a conjecture. Never upgraded by this layer.
evidencestr: Copied verbatim from verification["evidence"] ("none" when absent), or the free-text evidence supplied for a conjecture.
verificationdict: The full verification mapping, verbatim.
derivationtuple of dict: DerivedResult.steps.
certificatestr or None: Certificate source text, when one was emitted.
certificate_formatstr or None: Format of certificate, e.g. "lean4".
depends_ontuple of str: IDs of the claims this one was derived from.
checkdict or None: Machine-readable re-verification recipe (see ClaimGraph.verify()).
provenancedict: Identity-neutral but reproducible metadata: operation, argument renderings, Alkahest version, build feature flags.
recorded_atstr or None: ISO-8601 UTC timestamp. Volatile — excluded from to_json(stable=True) and from the graph digest.
audittuple of dict: Re-verification outcomes appended by ClaimGraph.verify().
labelstr or None: Short human-readable name used in rendered documents.
tagstuple of str: Free-form labels for querying.
notesstr or None: Free-form prose attached by the loop author.

Properties

id: str

statement: str

kind: str

latex: str | None

hypotheses: tuple[str, ...]

method: str

status: str

evidence: str

verification: dict[str, Any]

derivation: tuple[dict[str, Any], ...]

certificate: str | None

certificate_format: str | None

depends_on: tuple[str, ...]

check: dict[str, Any] | None

provenance: dict[str, Any]

recorded_at: str | None

audit: tuple[dict[str, Any], ...]

label: str | None

tags: tuple[str, ...]

notes: str | None

machine_checked: bool

True when a checker actually verified this claim.

An emitted-but-unchecked Lean certificate is not machine-checked.

badge: str

Honest one-line description of this claim's verification status.

mark: str

Short all-caps marker, e.g. "[VERIFIED]" or "[UNVERIFIED]".

Methods

content_id() → str

Recompute the content-addressed ID from this claim's own fields.

to_dict(*, stable: bool=False) → dict[str, Any]

Return a JSON-ready mapping.

Parameters

stablebool: When true, omit volatile fields (recorded_at and any audit timestamps) so that two runs of the same computation produce byte-identical output.

from_dict(data: Mapping[str, Any]) → Claim

classmethod

Rebuild a Claim from to_dict() output.

class

class research.ClaimGraph(
    *,
    title: str | None=None,
    metadata: Mapping[str, Any] | None=None
)

A cycle-free, content-addressed set of Claim records.

A graph owns its claims and their dependency edges. Edges always point from a claim to claims that already exist in the graph, which makes cycles impossible by construction for graphs built incrementally; graphs loaded from JSON are topologically checked at load time.

Parameters

titlestr, optional: Document title used by the renderers.
metadatamapping, optional: Free-form session metadata (build features, seeds, notes).

Examples

Python

>>> from alkahest.research import ClaimGraph
>>> g = ClaimGraph(title="Notes")
>>> len(g)
0

Properties

title: str | None

Document title used by to_markdown() / to_latex().

metadata: dict[str, Any]

Mutable free-form session metadata.

claims: tuple[Claim, ...]

All claims, in insertion order (which is a topological order).

ids: tuple[str, ...]

All claim IDs, in insertion order.

Methods

get(key: str, default: Claim | None=None) → Claim | None

Return the claim with this ID, or default.

add(claim: Claim) → Claim

Insert claim, or merge it into an identically-identified claim.

Because IDs are content-addressed, re-deriving the same claim is not an error: the stored claim keeps its original status and derivation and gains any new dependency edges, tags, and audit entries. Self-edges (a claim that cites an identically-addressed claim, which happens when an operation is a no-op) are dropped.

A re-verification recipe on the later claim is adopted when the stored claim carries none. Attaching a check is the one supported way to link a statement to evidence, so recording a statement bare and then recording it again with a recipe has to work; dropping the recipe made verify() report skipped for a claim that was in fact checkable. An existing recipe is never overwritten — the first recorded evidence wins, as the status does.

Raises

MissingClaimError: If any dependency is absent from the graph.
CycleError: If the edge would make the graph cyclic.

merge(other: ClaimGraph) → ClaimGraph

Return a new graph containing the claims of both graphs.

other's claims are inserted in its own topological order, so cross- graph citations resolve as long as the union is acyclic.

dependencies(key: str) → tuple[str, ...]

Direct dependencies of the claim with this ID.

dependents(key: str) → tuple[str, ...]

Claims that cite the claim with this ID directly.

ancestors(key: str) → tuple[str, ...]

All claims this one transitively rests on, nearest first.

impact(key: str) → tuple[str, ...]

Claims that would be invalidated if this claim turned out false.

The transitive closure of dependents() — the answer to "what depends on this claim if it turns out to be wrong?".

by_status(status: str) → tuple[Claim, ...]

All claims whose status equals status.

by_tag(tag: str) → tuple[Claim, ...]

All claims carrying tag.

by_method(method: str) → tuple[Claim, ...]

All claims produced by method.

machine_checkable() → tuple[Claim, ...]

Claims a checker actually verified (see Claim.machine_checked).

unverified() → tuple[Claim, ...]

Claims carrying no verification evidence at all.

roots() → tuple[Claim, ...]

Claims with no dependencies.

leaves() → tuple[Claim, ...]

Claims nothing else depends on.

summary() → dict[str, int]

Claim counts by status, sorted by status name.

topological_order() → tuple[str, ...]

A dependency-respecting ordering of the claim IDs.

to_dict(*, stable: bool=False) → dict[str, Any]

Return the graph as a JSON-ready mapping.

Claims are emitted in insertion (topological) order; every mapping is written with sorted keys by to_json().

to_json(*, indent: int | None=2, stable: bool=False) → str

Serialise to JSON with deterministic key order.

Parameters

indentint or None: Passed to json.dumps(). None emits a compact document.
stablebool: When true, drop volatile fields (timestamps, working directory) so two runs of the same computation produce byte-identical output. Identity — the claim IDs — never depends on volatile data, so a stable=False document still diffs cleanly outside those fields.

Examples

Python

>>> from alkahest.research import ClaimGraph
>>> ClaimGraph().to_json(indent=None, stable=True).startswith('{"claims": []')
True

from_dict(data: Mapping[str, Any]) → ClaimGraph

classmethod

Rebuild a graph from to_dict() output.

Raises

ClaimGraphError: On an unknown document kind or a schema version this build cannot read.
CycleError: If the dependency edges contain a cycle.

from_json(text: str) → ClaimGraph

classmethod

Rebuild a graph from to_json() output.

save(path: str | os.PathLike[str], *, stable: bool=False) → None

Write the graph to path as JSON (UTF-8, trailing newline).

load(path: str | os.PathLike[str]) → ClaimGraph

classmethod

Read a graph previously written by save().

digest() → str

SHA-256 of the stable serialisation — a fingerprint of the content.

Two runs of the same computation produce the same digest even though their timestamps differ.

verify(
    *,
    pool: Any=None,
    tolerance: float=1e-08,
    samples: Sequence[float]=(0.37, 1.23, 2.71),
    mark_refuted: bool=True
) → VerificationReport

Re-check every claim that carries a re-verification recipe.

Claims are re-derived from their serialised text — the recipe is parsed into a fresh ExprPool — so a graph loaded from disk can be revalidated against a newer library build rather than trusted blindly.

This pass can only lower confidence. A failed re-check marks the claim "refuted" (when mark_refuted); a successful one appends an audit entry and leaves the status alone.

Parameters

poolExprPool, optional: Pool to parse into. A fresh pool is created when omitted.
tolerancefloat: Absolute tolerance for the numeric residual fallback. It does not apply to a numeric_relation recipe whose constants are supplied at a precision a float cannot hold: those are evaluated exactly and judged against the precision the caller actually gave (see below).
samplessequence of float: Sample points used for the numeric fallback. Each sample gives a point, not a single value: free symbols are bound to the sample offset by their rank in sorted name order, so they take distinct values and the evaluation is off the diagonal x = y = z. A numeric_ok outcome is still finitely many points — evidence, never a proof — and a symbol whose offset leaves an operation's domain makes that point unevaluable, which the detail string reports and which can leave the outcome inconclusive.
mark_refutedbool: When true (default), failed claims have their status set to "refuted" in place.

Returns

VerificationReport

to_markdown(
    *,
    include_derivations: bool=True,
    include_certificates: bool=False,
    max_steps: int=12
) → str

Render the graph as a Markdown research document.

Every claim gets its statement, hypotheses, method, dependency links, derivation, and an honest verification badge. A summary table at the top states exactly which subset of the document a machine actually checked.

Parameters

include_derivationsbool: Emit the per-claim rewrite-step table.
include_certificatesbool: Inline the certificate source (can be long).
max_stepsint: Truncate derivation tables to this many steps.

to_latex(
    *,
    standalone: bool=True,
    include_derivations: bool=True
) → str

Render the graph as a LaTeX research document.

Each claim becomes a numbered subsection carrying \label{clm:<id>}; dependencies are emitted as \hyperref links, so a loop that ran for a week emits a writeup with every claim linked to its derivation and its certificate status.

Parameters

standalonebool: Emit a full article document (preamble + \begin{document}) rather than only the body.
include_derivationsbool: Emit the per-claim derivation list.

class

class research.RecheckOutcome

Result of re-checking one claim.

outcome is one of

"ok" The claim was re-established exactly (symbolic residual is zero). "numeric_ok" The exact check was inconclusive but a numeric residual check passed. This is evidence, not a proof. "failed" The re-check contradicts the claim. ClaimGraph.verify() marks such claims "refuted". "inconclusive" The recipe ran but decided nothing (e.g. the simplifier could not reduce the residual and no numeric sample was possible). "skipped" No re-verification recipe is attached to the claim.

Properties

claim_id: str

outcome: str

kind: str

detail: str

ok: bool

True when the re-check did not contradict the claim.

class

class research.ResearchSession(
    *,
    title: str | None=None,
    pool: Any=None,
    assumptions: Any=None,
    capture: bool=False,
    normalize: bool=True,
    graph: ClaimGraph | None=None,
    metadata: Mapping[str, Any] | None=None,
    crosscheck: bool=False
)

Records the results produced inside a block as a ClaimGraph.

Enter the session with session(). Inside the block:

with capture=True, every DerivedResult returned by a module-level Alkahest operation is recorded automatically, and its dependency edges are inferred from the expressions it was computed from;
record() registers a result explicitly (one line, always complete);
conjecture() registers a claim that is not proved — its status is hard-wired to "unverified".

Parameters

titlestr, optional: Document title.
poolExprPool, optional: Entered as the active context() pool for the block.
assumptionsAssumptions, optional: Hypotheses attached to every claim recorded in the block, and entered as the active assumption context. Defaults to whatever active_assumptions() reports at record time.
capturebool: Enable automatic capture (see captured_operations() for its exact scope).
normalizebool: Put expression statements into the kernel's normal form before hashing. Disable for very hot loops; IDs then depend on how the expression was built.
graphClaimGraph, optional: Continue an existing graph — this is how iteration N+1 cites iteration N.
metadatamapping, optional: Extra session metadata stored on the graph.

Methods

record(
    result: Any,
    *,
    statement: Any=None,
    method: str | None=None,
    label: str | None=None,
    hypotheses: Sequence[str] | None=None,
    depends_on: Sequence[str]=(),
    sources: Sequence[Any]=(),
    tags: Sequence[str]=(),
    notes: str | None=None,
    check: Mapping[str, Any] | None=None,
    arguments: Sequence[str] | None=None,
    crosscheck: Any=None
) → Claim

Record a DerivedResult (or bare Expr) as a claim.

The claim's status, evidence, and certificate are copied verbatim from result.verification; this method never upgrades them.

Parameters

resultDerivedResult or Expr

The result to record.

statementExpr, DerivedResult, str or mapping, optional

What the claim asserts, if different from result.value. A mapping of the form {"kind": ..., "statement": ..., "latex": ...} is used verbatim, which is how relations such as ∫ f dx = F are supplied.

It is free text, and nothing checks that it describes result. So a machine-checked status is not carried over onto it: when statement is supplied without a check recipe and the result's status is in MACHINE_CHECKED_STATUSES, the claim is stored as "asserted" instead, with the result's own status preserved under verification["result_status"]. Supply check — the recipe ClaimGraph.verify() re-runs — to keep the machine-checked status, or record the result without statement.

methodstr, optional

Operation name. Defaults to "record".

labelstr, optional

Short human-readable title for rendered documents.

hypothesessequence of str, optional

Overrides the hypotheses taken from the active Assumptions.

depends_onsequence of str

Explicit dependency claim IDs.

sourcessequence

Expressions or results this was computed from; their originating claims (if recorded in this session) become dependency edges.

tags, notesoptional

Free-form metadata.

checkmapping, optional

A re-verification recipe (see ClaimGraph.verify()).

argumentssequence of str, optional

Rendered arguments stored in the claim's provenance.

crosscheckCrossCheck, optional

An already-computed crosscheck.CrossCheck, attached to the claim under verification["crosscheck"] and surfaced as a crosscheck:<outcome> tag.

It is evidence, never a verdict. Agreement with an independent implementation does not upgrade the status, and a divergence does not set "refuted" either: a divergence names two suspects, not one (P2-2 design decision D5), so which side is wrong is for a human or a later check to adjudicate. The recording layer's honesty invariant — it may never raise confidence — is preserved exactly.

Returns

Claim: The stored claim (merged, if an identical claim already existed).

conjecture(
    statement: Any,
    *,
    evidence: str,
    method: str='conjecture',
    label: str | None=None,
    hypotheses: Sequence[str] | None=None,
    depends_on: Sequence[str]=(),
    sources: Sequence[Any]=(),
    tags: Sequence[str]=(),
    notes: str | None=None,
    check: Mapping[str, Any] | None=None
) → Claim

Record a claim that is not proved.

The status is hard-wired to "unverified" — there is deliberately no parameter to say otherwise. evidence is free text describing why the conjecture is plausible (e.g. "PSLQ at 60 digits"); it is rendered as supporting evidence, never as a proof.

Returns

Claim

cite(claim: str | Claim) → Claim

Mark a claim as a dependency of the next result recorded.

Lets iteration N+1 cite iteration N by ID even when the two are not linked by a shared expression object.

Raises

MissingClaimError: If the ID is not in this session's graph.

run(operation: Callable[..., Any], *args: Any, **kwargs: Any) → Any

Call operation and record its result, returning the result.

The explicit, always-complete alternative to automatic capture: dependency edges are inferred from args exactly as they would be by the capture hook.

Python

>>> import alkahest as ak                      # doctest: +SKIP
>>> value = s.run(ak.integrate, f, x)          # doctest: +SKIP

capture_report() → dict[str, Any]

What automatic capture is doing, and anything it could not do.

Returns a mapping with mode, the operations currently hooked, the number of claims recorded, and any errors raised inside the hook.

class

class research.VerificationReport

Aggregate outcome of ClaimGraph.verify().

Properties

outcomes: tuple[RecheckOutcome, ...]

alkahest_version: str

checked_at: str | None

ok: bool

True when no claim was refuted.

failed: tuple[RecheckOutcome, ...]

Outcomes that contradicted their claim.

Methods

summary() → dict[str, int]

Count of outcomes by kind, e.g. {"ok": 3, "skipped": 2}.

to_markdown() → str

Render the report as a Markdown table.

exception

exception research.ClaimGraphError(ValueError)

Base class for claim-graph errors (E-RESEARCH-*).

exception

exception research.CycleError(ClaimGraphError)

The deserialised graph contains a dependency cycle.

exception

exception research.MissingClaimError(ClaimGraphError, KeyError)

A dependency edge referenced a claim that is not in the graph.

function

research.captured_operations() → tuple[str, ...]

Operations currently wrapped for automatic capture.

Empty until the first session() with capture=True is entered. Automatic capture sees calls made through the module namespace (alkahest.integrate(...)). It does not see calls through a name bound before the hooks were installed (from alkahest import integrate) or methods on objects (Assumptions.simplify); use ResearchSession.record() for those.

function

research.claim_id(
    statement: str,
    hypotheses: Sequence[str]=(),
    method: str=''
) → str

Return the content-addressed identifier for a claim.

The identifier is "clm_" + sha256(payload)[:16] where payload is a canonical JSON encoding of the normalised statement, the sorted set of hypotheses, and the method. It deliberately does not include timestamps, dependency edges, or the library version, so the same claim derived twice in different sessions receives the same ID.

Parameters

statementstr: The already-normalised statement text (see ResearchSession.record(), which normalises for you).
hypothesessequence of str: Hypothesis predicates. Order is irrelevant — they are sorted.
methodstr: The operation or method that produced the claim, e.g. "integrate".

Returns

str: A stable identifier such as "clm_9f1c0b2a7d4e5f60".

Examples

Python

>>> from alkahest.research import claim_id
>>> claim_id("(1/2 * log(2))", ["x > 0"], "integrate") == claim_id(
...     "(1/2 * log(2))", ["x > 0"], "integrate"
... )
True

function

research.session(
    *,
    title: str | None=None,
    pool: Any=None,
    assumptions: Any=None,
    capture: bool=False,
    normalize: bool=True,
    graph: ClaimGraph | None=None,
    metadata: Mapping[str, Any] | None=None,
    crosscheck: bool=False
) → ResearchSession

Open a research session (see ResearchSession).

Python

>>> import alkahest as ak
>>> pool = ak.ExprPool()
>>> x = pool.symbol("x")
>>> with ak.research.session(title="Demo", pool=pool, capture=True) as s:
...     _ = ak.integrate(x, x)
>>> len(s.graph)
1

constant

research.MACHINE_CHECKED_STATUSES

MACHINE_CHECKED_STATUSES = frozenset({'exactly_verified', 'lean_checked'})

No docstring.

constant

research.SCHEMA_VERSION

SCHEMA_VERSION = 1

No docstring.

constant

research.STATUS_BADGES

STATUS_BADGES = {'lean_checked': 'an external Lean 4 run checked this claim', 'exactly_verified': 'the kernel proved the symbolic residual is zero', 'certificate_available':…

No docstring.