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

# The Lemma Hub flywheel, measured

> Eleven sequential verifications on one machine: what the Lemma Hub changes, and what it does not.

This experiment starts from an empty Lemma Hub and an empty lemma cache, and runs one `theformalera verify` per step. Each step is a new program (new IR, so no result-cache hit), and the Hub's admission check runs between steps. "Value subgoal" is the time `tfe_close` spent inside Lean closing the certificate's value subgoal.

| Step | Target (`mlp.act` unless noted) | Lemma Hub | Verdict | Value subgoal | Lemmas hit | New lemmas |
| - | - | - | - | - | - | - |
| 0 | Impl A, config 1 (tanh-based sigmoid) | disabled | **UNKNOWN** (subgoal left open) | 880 ms | 0 | 0 |
| 1 | Impl A, config 1 | built-ins, empty library | PROVED (search) | 762 ms | 2 built-in | 1 → acme (`L-d07f2c`) |
| 2 | Impl A, config 2 | online deposit | PROVED (hit) | 213 ms | `L-d07f2c` + 1 built-in | 0 |
| 3 | Impl A, config 3 | ″ | PROVED (hit) | 237 ms | ″ | 0 |
| 4 | Impl A, config 4 | ″ | PROVED (hit) | 217 ms | ″ | 0 |
| 5 | Impl B: another team's agent; other layout, operation order, tile 2048 | org library | PROVED (hit) | 207 ms | ″ | 0 |
| 6 | Impl B, tile 256 | ″ | PROVED (hit) | 259 ms | ″ | 0 |
| 7 | Impl A on **Qwen/Qwen3-0.6B** (`I = 3072`) | ″ | PROVED (hit) | 247 ms | ″ | 0 |
| 8a | RMSNorm via `√(1/v)`, Qwen3.8-27B `input_norm` | ″ | PROVED (search) | 1541 ms | 2 built-in | 1 operator-level (`L-953f36`, `H` and `ε` symbolic) |
| 8b | The same kernel on **Muse-Glimmer-30B** (`H = 6656`, `ε = 1e-5`) | ″ | PROVED (hit) | 985 ms | `L-953f36` + 2 built-in | 0 |
| 8c | Negative control: the `(1 + w)` kernel on granite-4.2-3b, whose spec uses `w` | ″ | **FAILED** | — | 0 | 0 |

![Bar chart of the time to close the value subgoal: 880 ms not closed with the Hub off, 762 ms closed by search, then 207 to 259 ms closed by a Lemma Hub hit for later configs, another implementation and another model](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/charts/flywheel-solver-time.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=aa0468257cd0b5e16e63422ebac420d4)

## What it shows

1. **With the Hub off, the kernel is UNKNOWN; with it on, it is PROVED.** Without the built-in identity `tanh_eq_exp`, generic search (`ring_nf`, `field_simp`, the exp / sinh / cosh rewrites) cannot close the tanh-SiLU subgoal. The verdict is UNKNOWN, never PASS.
2. **Once a lemma is deposited, later verifications hit instead of searching.** The value subgoal drops from 762 ms to 204–259 ms (3–3.7×) for every later autotune config, for another team's implementation with a different layout and operation order, and for a different model. This works because the canonical subgoal ignores tile sizes, code layout, operation order and, for operator-level lemmas, the model constants.
3. **Operator-level lemmas cross model families.** The RMSNorm lemma was proved with `H` and `ε` symbolic on Qwen3.8-27B, and hit on Muse-Glimmer-30B.
4. **Lemmas change speed, never verdicts.** A kernel that is wrong for its model (8c) is FAILED, with the same counterexample, however full the library is.

![Bar chart: the RMSNorm value subgoal takes 1541 ms by search on Qwen3.8-27B and 985 ms by a Lemma Hub hit on Muse-Glimmer-30B](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/charts/cross-model-operator-lemma.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=94d26c89919046c405ce1cccdfbb98ef)

## What it does not show

* **The scale is seconds, not minutes.** A whole proof check of these kernels takes about 3 s, of which about 2.1 s is Lean loading Mathlib. The Lemma Hub's effect today is UNKNOWN → PROVED, plus a 3–4× faster value subgoal. It is not yet visible as minutes saved per kernel.
* End-to-end wall time per step is 3.4–12.7 s, dominated by lowering and Lean start-up. Steps 2 and 8b also compile the lemma pack once (4.6–4.8 s, cached afterwards).
* The structural lemmas where the savings should be large (online softmax, split-KV merge, the chunked delta rule) are proved and audited, but not wired into the proof generator yet. Attention and Gated DeltaNet kernels stay UNKNOWN for now.

## At scale: 48 organisations, 319 kernels

The same mechanism, measured across a community instead of one node. Sixteen organisations, then 32 more, verify their own Triton kernels for the seven public models against one shared Lemma Hub: 382 configurations in all, on NVIDIA sm\_80 to sm\_100a and AMD gfx942 / gfx950. Each one is compared with the same project verified against an empty library.

The metric that matters is how fast the N-th independent implementation of an operator verifies:

| N-th implementation | Value subgoals | Median time | Closed by a hit |
| - | - | - | - |
| 1st | 6 | 802 ms | 0% |
| 2nd–3rd | 11 | 340 ms | 55% |
| 4th–7th | 23 | 222 ms | 65% |
| 8th–15th | 32 | 223 ms | 84% |
| 16th–31st | 40 | 300 ms | 73% |
| 32nd–63rd | 42 | 262 ms | 93% |

![Two bar charts by the N-th implementation of an operator: median value-subgoal time falls from 802 ms for the first implementation to 222–300 ms afterwards, and the share closed by a Lemma Hub hit rises from 0% to 93%](https://mintcdn.com/n-a-24de7f09/Rgs46GF-p6gIpda5/images/charts/scale-nth-implementation.png?fit=max\&auto=format\&n=Rgs46GF-p6gIpda5\&q=85\&s=34a75a13bfc87cda550dad687a6582c1)

* Over all 48 users, 116 of 154 non-trivial value subgoals (75%) are closed by a lemma someone else deposited, and the time spent on them is halved.
* New idioms show up as a dip: users 17–24 bring norm and GELU forms nobody had written, and the hit share falls before the community's deposits bring it back.
* The public library holds 23 lemmas at the end. Lemmas deposited by NVIDIA projects close the subgoals of AMD projects, because a lemma statement never mentions the target.
* All 382 configurations get the same verdict with and without the community: 313 PROVED, 49 real bugs FAILED, 16 UNKNOWN.

The data, scripts and every run's JSON report are in `supporting-materials/` (`dataset/scale/`, `logs/scale/`, `scripts/scale.py`).

## Reproduce it

The per-step JSON reports are in `supporting-materials/logs/flywheel-runs/`. The script that sets up a fresh Hub and runs every step is `supporting-materials/scripts/flywheel.py`:

```bash theme={"system"}
uv run python supporting-materials/scripts/flywheel.py
```


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