> ## 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 Hub
> How reusable sub-proofs are retrieved before solving and deposited after, and why they change speed but never verdicts.
Spec Hub stores **what** to compute. The Lemma Hub stores **how to prove** it was computed correctly. When a proof needs a sub-proof that took search to find, that sub-proof becomes a lemma. The next verification that meets the same subgoal cites the lemma instead of searching again. That includes another autotune config, another team's kernel for the same node, or another model that uses the same operator.
## What a lemma looks like
A lemma is a Lean 4 theorem plus metadata. Its statement is a canonical equation over the reals. It mentions only arithmetic, numerals and `Real.*` functions, never a kernel, a file, a repository or a variable name.
```text theme={"system"}
$ theformalera lemma show L-d07f2c
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
```
This lemma says that a SiLU written with `tanh` (`g · (1 + tanh(g/2)) / 2 · u`) equals the spec's `g · σ(g) · u`. The id is a hash of the statement, so the same subgoal from two kernels, two configs or two organisations is the same lemma.
## Scope
| Scope | The statement mentions | Who can hit it |
| - | - | - |
| `general` | Only Mathlib, no model constant | Any kernel of any model |
| `operator` | An Op Spec's algebra, with the model constants turned into variables | Any model that uses the operator |
| `model` | Concrete constants of one model | Other implementations of the same model |
Constants that a proof never needs to unfold become variables when the lemma is extracted. That is how an RMSNorm lemma first proved for Qwen3.8-27B (`H = 5120`, `ε = 1e-6`) hits on Muse-Glimmer-30B (`H = 6656`, `ε = 1e-5`). See [The Lemma Hub flywheel](https://docs.theformalera.com/case-studies/lemma-flywheel.md).
## The online flow
```mermaid theme={"system"}
flowchart LR
fetch["Retrieve
by the run's Op Specs"]
pack["Pack
regenerate, compile locally,
axiom-check"]
solve["Solve
hit first, search on a miss"]
route["Route
public / org / local / nowhere"]
admit["Admit
Hub-side Lean re-check"]
hub[("Lemma Hub")]
fetch --> pack --> solve --> route --> admit --> hub
hub -. "next verification" .-> fetch
```
1. **Retrieve.** Before solving, the CLI asks for the lemmas of the run's Op Specs, plus the general ones, from the libraries in `[lemmas] use`. Only op names and Spec Keys leave the machine, never kernel source.
2. **Pack.** Each retrieved record is regenerated from a fixed template. Its statement and proof name are validated against an allowlist. Everything is compiled locally into one Lean module, and its axioms are checked. A lemma that fails is dropped, never trusted.
3. **Solve.** For each value subgoal, `tfe_close` first tries `ring_nf` (a goal it closes is *trivial* and is never stored). Then it tries a hit in the pack, and only then a portfolio of tactics.
4. **Route.** New lemmas go where `[lemmas] contribute` says; open goals (subgoals nothing closed) are reported the same way.
5. **Admit.** On the Hub, every deposit is regenerated, compiled against the Hub's own spec package, checked against the axiom allowlist, and deduplicated (the fastest proof is kept). Its visibility is re-derived on the Hub side.
UNKNOWN runs deposit too: whatever they proved before giving up is kept, and the subgoals they could not close are reported as open goals.
## Seeing the effect
Every run ends with the Lemma Hub line:
```text theme={"system"}
lemma hub: 2 hits (1 acme · 1 built-in) · ~600ms solver time saved · 0 new
```
* **hits** are counted per library (`built-in`, `public`, your org, `local`).
* **solver time saved** is estimated as the first-solve time of each lemma that was hit.
* **new** lemmas are listed with their destination: `1 new → acme`.
The same numbers are in the JSON report (`lemmas.hits`, `lemmas.saved_s`, `lemmas.new`) and in the GitHub Action's outputs.
## Where lemmas go
```toml theformalera.toml theme={"system"}
[lemmas]
use = ["public", "org"] # which libraries to search
contribute = "org" # off | org | public: where lemmas from this project go
snapshot = "latest" # or a snapshot time, to reproduce the solving process bit for bit
```
| `contribute` | Effect |
| - | - |
| `off` | Nothing is uploaded. With `runner = "local"`, lemmas are still kept in this repository's CI cache (`.theformalera/lemmas/local`). |
| `org` | Uploaded to your organisation's library. |
| `public` | Lemmas built only from public definitions go to the public library; the rest go to the org library. |
If `contribute` is not set, the default depends on the tier and run mode:
| Scenario | Default |
| - | - |
| Free tier, `cloud` | `public` |
| Team or Enterprise, `cloud` | `org` |
| `local` | `off` |
| `on-prem` | `org` |
Three rules always apply:
* A lemma whose node belongs to a **private spec** only ever goes to the org library. No setting changes that.
* An organisation admin can set a **cap** on the Hub (for example, "no public contribution"). A repository's setting can only be stricter, never looser.
* Public lemmas do not record which organisation contributed them.
`theformalera lemma preview` lists what the last run deposits and where each lemma goes, before anything else reads it.
## Speed, never verdicts
* A lemma can only help the engine find a proof faster. It cannot manufacture one: every lemma has passed the Lean kernel, and the final certificate is checked by the Lean kernel again.
* FAILED comes from a concrete counterexample and has nothing to do with lemmas.
* So as the library grows, an UNKNOWN can become a PASS, and nothing else changes. Run `theformalera verify --no-lemmas` to see the baseline without the Lemma Hub.
## Proofs carry their lemmas
The Lean sources of every lemma a proof imports ship with it, in `proofs/lemmas/`, with a digest in the release certificate. When a customer re-checks a release, the lemmas are compiled from source first. The Lemma Hub is therefore **not** part of the trusted base: if it is wrong, tampered with or offline, the worst case is a slower verification.
## Built-in lemmas
The spec package ships proved structural lemmas in `TheFormalEra.Lemmas`:
| Lemma | Statement |
| - | - |
| `tanh_eq_exp` | `tanh x = (exp 2x − 1)/(exp 2x + 1)` |
| `exp2_eq_exp` | `2^y = exp (y · log 2)` (`tl.exp2`-based kernels) |
| `inv_mul_eq_inv_div` | `x⁻¹ · c = (x · c⁻¹)⁻¹` (`√(H / (Σx² + H·ε))` norms) |
| `inv_sqrt_mul_eq` | `(√v)⁻¹ · c = (√(v / c²))⁻¹` for `c > 0` (`√H / √(Σx² + H·ε)` norms) |
| `tiled_masked_sum` | A masked, tiled traversal covers `[0, n)` exactly once |
| `tiled_floor_misses` | `⌊n/B⌋` tiles miss the tail when `B ∤ n` |
| `online_softmax_rescale` | Online softmax rescaling by `exp(m − m')` |
| `splitKV_lse_merge` | Split-KV merging in log-sum-exp form equals full attention |
The last two are proved and audited, but not yet wired into the proof generator. See [Limitations](https://docs.theformalera.com/concepts/limitations.md).
This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.