Skip to main content
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.
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

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.

​
The online flow

  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:
  • 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

theformalera.toml
If contribute is not set, the default depends on the tier and run mode: 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: The last two are proved and audited, but not yet wired into the proof generator. See Limitations.