> ## 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 administration

> Admission, contribution caps, audit logs, snapshots, migration and statistics of a Hub's Lemma Hub.

## Admission

Deposits land in `lemmas/inbox/`. Nothing in them is trusted: admission re-derives everything.

```bash theme={"system"}
uv run theformalera-hub lemmas admit --store hub-data --specs specs
```

```text theme={"system"}
usage: folded 3 verification report(s) into the hit statistics
D-76ec659a2f (acme): 1 admitted, 0 rejected, 0 duplicates
  + L-d07f2c  general-level → org  (Lean re-check 2.32s)
```

For each deposited lemma, admission:

1. regenerates the Lean module from the fixed template. The statement may only use allowlisted identifiers (`Real.exp`, `Real.tanh`, `Real.sqrt`, `Real.log`, `Real.sinh`, `Real.cosh`, `ℝ` and bound variables), and the proof must be one of the search portfolio's tactic scripts. A module therefore cannot run commands, add axioms, or use `sorry` or `native_decide`;
2. compiles it with Lean against the Hub's own spec package;
3. checks the axioms of the compiled theorem: only `propext`, `Classical.choice` and `Quot.sound` are allowed;
4. checks that the id is the hash of the statement;
5. deduplicates: for an identical statement, the fastest proof is kept;
6. re-derives the visibility Hub-side. Lemmas of nodes passed as `--private-node` only ever go to the org library;
7. writes an audit-log entry.

On AWS, the Solver stack runs admission as a scheduled ECS task every 3 days.

## Contribution caps

```bash theme={"system"}
uv run theformalera-hub lemmas cap --store hub-data --org acme --cap org
```

A cap (`off`, `org` or `public`) is the loosest setting any repository of the organisation may use. A repository's `[lemmas] contribute` can only be stricter.

## Audit log

```bash theme={"system"}
uv run theformalera-hub lemmas audit --store hub-data --org acme
```

One JSON line per upload: the submission, the lemma ids, their destination and the outcome.

## Snapshots

```bash theme={"system"}
uv run theformalera-hub lemmas snapshot --store hub-data [--org acme]
```

This prints a snapshot time. A project that sets `[lemmas] snapshot = "<time>"` retrieves only lemmas created up to that time, which reproduces a solving process exactly.

## Migration

After a Lean or Mathlib upgrade:

```bash theme={"system"}
uv run theformalera-hub lemmas migrate --store hub-data --specs specs
```

Every lemma is re-checked against the workspace's toolchain. Failures are marked `pending-migration` and leave retrieval. Proofs already issued are unaffected, because they pin their own toolchain.

## Export

To move libraries to another Hub when there is no network path between them, write them to one deposit file:

```bash theme={"system"}
uv run theformalera-hub lemmas export --store hub-a --store hub-b --specs specs -o lemmas.json
```

```text theme={"system"}
Lean re-check against specs: 28 ok, 0 failed
wrote lemmas.json: 28 lemmas (9 general, 8 model, 11 operator) from 27 store(s), submission D-export-017cb8e1bf
```

The command reads the public and org libraries of every store (`--public-only` skips org libraries) and merges lemmas with the same statement. Lemmas pending migration are skipped. `--specs` re-checks every lemma with Lean before writing. Copy the file into the target Hub's `lemmas/inbox/` and run admission there. Admission re-checks everything again, because nothing in the file is trusted. The target Hub's spec package must contain the search-portfolio entries the proofs name; otherwise admission rejects those lemmas.

## Statistics

```bash theme={"system"}
uv run theformalera-hub lemmas stats --store hub-data [--org acme]
```

Library sizes by scope, total hits, and open goals per node: the subgoals no lemma or search closed. Open goals show which built-in lemmas are missing.


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