Python SDK

artano-lemma is the Python distribution of Lemma. It targets the same surface as the Node MCP server, but lets you read the corpus in-process from a notebook or script.

Install

pip install artano-lemma

The base install is deliberately light — httpx, pydantic, jsonschema, typer, rich, mcp. One optional extra adds symbolic verification:

pip install "artano-lemma[symbolic]"   # adds SymPy

Without it, symbolic verification degrades to recording the claim rather than erroring.

After install, a lemma command is on your PATH:

lemma verify ideal-gas-law --output '{"gasConstant_J_per_molK": 8.3145}'
lemma crosscheck ./my-draft-card.json
lemma paths                          # where the corpus + schema resolve
lemma list [--kind K] [--domain D]   # list cards
lemma show density-of-states         # pretty-print one card
lemma authors <card-id>              # who a card credits
lemma serve                          # run the MCP server over stdio

verify and crosscheck exit 0 when a check passes, 1 when the engine reports a HIGH severity, and 2 when they could not run at all — the same contract as the Node CLI, so either one drops into a pipeline the same way.

The one command that exists only here is crosscheck --symbolic, which proves declared limit and conservation claims instead of recording them:

$ lemma crosscheck lotka-volterra-with-logistic-prey
— 3 of 7 checks passed · severity LOW

$ lemma crosscheck lotka-volterra-with-logistic-prey --symbolic
— 7 of 7 checks passed · severity NONE

Use it from Python

from artano_lemma import load_cards

cards = load_cards()
print(f"{len(cards)} cards loaded")

# filter to one domain
condensed = [c for c in cards if (c.domain or "").startswith("physics-condensed-matter")]
for c in condensed:
    print(c.id, c.kind)

# inspect a single card
card = next(c for c in cards if c.id == "density-of-states")
print(card.name)

Pointing at a different corpus

By default the SDK reads the bundled corpus. Pass an explicit path (or set LEMMA_CARDS_DIR) to read a private fork or an unreleased card you are drafting:

from pathlib import Path
from artano_lemma import load_cards

cards = load_cards(Path("/path/to/your/cards"))

Verifying

The engine is available directly, without going through MCP. Three entry points, at three different relations:

from artano_lemma import (
    find_card, load_cards,
    run_usce_checks,          # does one run's output sit inside the card's envelopes?
    run_series_checks,        # does every reported sample satisfy the card's conditions?
    run_convergence_check,    # does the refinement study show the order the card claims?
    run_agreement_checks,     # do two independent methods agree, per the card's tolerances?
    run_hypothesis_checks,    # is a proposed new card consistent with the corpus?
)

cards = load_cards()
card = find_card(cards, "free-fall-uniform-gravity")

result = run_usce_checks({"gEarth_m_per_s2": 9.81}, card)
print(result.overall)
for check in result.checks:
    print(check.severity, check.detail)

An absent check is not a passing one

By default, an output key with no declared envelope is simply not checked, and the run can come back clean having verified nothing at all. Pass require_checks=True to make that state a finding instead:

run_usce_checks(output, card, require_checks=True)

Use it in CI, where “nothing was checked” and “everything passed” must not look alike.

Series conditions

Reaches cards an envelope cannot. A density of states has no system-independent magnitude — so density-of-states declares no envelopes at all — but it can never be negative:

card = find_card("density-of-states", cards)
run_series_checks({"epsilon": [-1, 0, 1], "g": [0.0, 1.2, 0.4]}, card)

Conditions come from the card’s seriesConditions; pass them explicitly only to explore a claim a card does not yet carry.

Convergence order

Recomputes the order from the refinement study rather than trusting a reported number:

card = find_card("finite-difference-truncation-error", cards)
run_convergence_check([(0.1, 1e-5), (0.05, 2.5e-6), (0.025, 6.25e-7)], card)

A study containing round-off-limited levels fits a shallower slope. That comes back as warn with the per-level orders attached, not fail — the method is fine and the measurement is contaminated, and those are different findings.

Cross-method agreement

run_agreement_checks(
    {
        "method-a": {"latticeConstant_A": 5.470},
        "method-b": {"latticeConstant_A": 5.475},
    },
    card,
)

Each observable the card declares a tolerance for, and that at least two methods report, is tested for spread. A single method raises rather than passing — it cannot corroborate itself. See cross-method agreement for the card side.

Symbolic verification

A hypothesis card may declare that in some regime its formula reduces to something known — “as b → 0, this reduces to free-fall-uniform-gravity”. By default the engine records that claim and returns warn: it confirms the claim is well-formed and does not pretend to have tested it.

With SymPy installed, the claim can actually be discharged:

run_hypothesis_checks(card, corpus=cards, symbolic=True)

This covers the machine-readable claims — limits, substitutions, roots, fixed points of coupled systems, and the rate at which a declared quantity evolves.

Three properties of this feature are worth knowing before you rely on it:

It is off by default, and stays that way. Turning it on changes what a verdict means, so it is opt-in for the same reason require_checks is: existing results were produced under the recorded behaviour, and silently re-baselining them would be worse than the missing capability.

It is Python-only. There is no comparable computer-algebra system in the Node ecosystem, so the MCP server does not have this and will not get it. This is the one deliberate divergence between the two implementations; everything else is contracted to produce byte-identical output in both.

It refuses rather than guesses. A limit that will not evaluate, a target that will not resolve, or a comparison the algebra system cannot decide all return warn. Only a difference shown to be non-zero returns fail. Cannot check and checked, and it is wrong never share a code path — an unproven claim is not a disproven one.

Status

The cards loader, the lemma CLI, and the full cross-check engine are usable today. The Python and Node engines are held to byte-identical verdicts and byte-identical prose by a shared fixture, so either one is a valid production choice; pick by which runtime you already have. The symbolic adapter above is the sole documented exception.

artano-lemma is at 0.1.0. Apache-2.0.

The full public API surface — typed card models, the validator, the corpus loader, the engine, and the MCP client — is documented in the package source under sdk-py/.