Skip to main content

​
Admission

Deposits land in lemmas/inbox/. Nothing in them is trusted: admission re-derives everything.
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

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

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

​
Snapshots

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

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.