Lemma commands - The Formal Era

lemma show

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.

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

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.

$ 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

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

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:

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.

⌘I