> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Lemma commands

> lemma show, lemma search, lemma list and lemma preview.

## lemma show

```bash theme={"system"}
theformalera lemma show LEMMA_ID [--json]
```

Show one lemma: its source and scope, the library it lives in, the statement (rendered and in Lean), the proof, its nodes, references, toolchain, first-solve time and usage. Lemmas are looked up on the Hub, then in this repository's CI cache.

```text theme={"system"}
L-d07f2c  online-deposited · general-level · acme library (org)

Statement    ∀ (a0 a1 : ℝ), a0 * a1 * (1/2) + a0 * a1 * tanh (a0 * (1/2)) * (1/2) = a0 * a1 * (1 + exp (-a0))⁻¹
Lean         ∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1 / 2 : ℝ)) * (1 / 2 : ℝ) = a0 *
             a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹
Proof        tfe_replay "tanh_eq_exp; exp_neg; field_simp; ring_nf"
Nodes        Qwen/Qwen3.8-27B:mlp.act
References   Mathlib (Real.*) only — no kernel, file or spec definition
Toolchain    leanprover/lean4:v4.35.0 · mathlib v4.35.0
First solve  559ms
Usage        referenced by 0 projects · 0 hits in total
```

## lemma search

```bash theme={"system"}
theformalera lemma search [QUERY] [--key SPEC_KEY] [--op OP_SPEC] [--json]
```

Search the public library and your org library. With `--key`, the node's Op Spec is looked up in the locked spec, and lemmas for that operator are listed. These are the implementation patterns that already verify fast.

```text theme={"system"}
$ theformalera lemma search --key 'Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act'
 id         scope     library   statement                                                  hits   first solve
 ────────────────────────────────────────────────────────────────────────────────────────────────────────────
 L-d07f2c   general   org       ∀ (a0 a1 : ℝ), a0 * a1 * (1/2) + a0 * a1 * tanh (a0 *      0      559ms
                                (1/2)) * (1/2) = a0 * a1 * (1 + exp (-a0))⁻¹
```

## lemma list

```bash theme={"system"}
theformalera lemma list [--json]
```

For each (kernel, node, config) of the last run: the lemmas it hit (or `cached`), the lemmas it deposited, and the number of open goals. The table ends with the run's Lemma Hub line.

## lemma preview

```bash theme={"system"}
theformalera lemma preview [--json]
```

What the last run deposited and where each lemma goes, with rendered statements, the contribution policy in force, the open goals and the submission id:

```text theme={"system"}
contribution policy: contribute = "org" · runner local · snapshot 2026-11-01T04:10Z
L-d07f2c  general-level  →  acme library (org)
  ∀ (a0 a1 : ℝ), a0 * a1 * (1/2) + a0 * a1 * tanh (a0 * (1/2)) * (1/2) = a0 * a1 * (1 + exp (-a0))⁻¹
  first solved in 559ms by `tanh_eq_exp; exp_neg; field_simp; ring_nf` · nodes Qwen/Qwen3.8-27B:mlp.act
submitted as D-76ec659a2f: queued for the Hub-side Lean re-check (admission)
```

The record is kept in `.theformalera/lemmas/last-deposit.json`.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.