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

# Deposit lemmas

> Queue new lemmas and open goals for admission. Nothing is trusted as submitted: the admission task regenerates every lemma from the template, compiles it with Lean against the Hub's spec package, enforces the axiom allowlist and re-derives the visibility. At most 500 lemmas and 500 open goals, 8 MiB.



## OpenAPI

````yaml /api-reference/openapi.json post /v1/lemmas/deposit
openapi: 3.1.0
info:
  title: Spec Hub API
  version: '1'
  description: >-
    The registry of Lean 4 specification packages, the cloud verification queue
    and the Lemma Hub. The `theformalera` CLI is the main client; this API is
    what it calls.
servers:
  - url: https://hub.theformalera.com
    description: Spec Hub
  - url: http://127.0.0.1:8700
    description: Local Hub (`theformalera-hub serve`)
security: []
tags:
  - name: Registry
    description: 'Public: no token needed.'
  - name: Verification
    description: Cloud solving (`runner = "cloud"`).
  - name: Lemma Hub
    description: Lemma retrieval, deposit and usage statistics.
paths:
  /v1/lemmas/deposit:
    post:
      tags:
        - Lemma Hub
      summary: Deposit lemmas
      description: >-
        Queue new lemmas and open goals for admission. Nothing is trusted as
        submitted: the admission task regenerates every lemma from the template,
        compiles it with Lean against the Hub's spec package, enforces the axiom
        allowlist and re-derives the visibility. At most 500 lemmas and 500 open
        goals, 8 MiB.
      operationId: lemma_deposit_v1_lemmas_deposit_post
      parameters: []
      requestBody:
        required: true
        content:
          application/json:
            schema:
              type: object
              properties:
                lemmas:
                  type: array
                  items:
                    $ref: '#/components/schemas/Lemma'
                  description: >-
                    New lemmas (id, statement, proof, scope, nodes, visibility,
                    …).
                open_goals:
                  type: array
                  items:
                    type: object
                    properties:
                      statement:
                        type: string
                        description: Unclosed canonical subgoal.
                      node:
                        type: string
                        description: Spec Key.
                  description: Subgoals no lemma or search closed.
                snapshot:
                  type: string
                  description: Lemma snapshot the run used.
                toolchain:
                  type: string
                  description: Engine / toolchain of the run.
      responses:
        '202':
          description: Accepted.
          content:
            application/json:
              schema:
                type: object
                properties:
                  submission:
                    type: string
                    description: Submission id.
                    example: D-76ec659a2f
                  status:
                    type: string
                    description: Always `queued`.
                  lemmas:
                    type: integer
                    description: Lemmas received.
              example:
                submission: D-76ec659a2f
                status: queued
                lemmas: 1
        '401':
          description: Missing or invalid bearer token.
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
        '413':
          description: Deposit larger than 8 MiB.
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
      security:
        - bearerAuth: []
components:
  schemas:
    Lemma:
      type: object
      properties:
        schema:
          type: string
          description: Record schema.
          example: theformalera.lemma/v1
        id:
          type: string
          description: 'Lemma id: a hash of the canonical statement.'
          example: L-d07f2c
        statement:
          type: string
          description: Canonical statement in Lean 4 (Mathlib identifiers only).
          example: >-
            ∀ (a0 a1 : ℝ), a0 * a1 * (1 / 2 : ℝ) + a0 * a1 * Real.tanh (a0 * (1
            / 2 : ℝ)) * (1 / 2 : ℝ) = a0 * a1 * ((1 : ℝ) + Real.exp (-a0))⁻¹
        pretty:
          type: string
          description: Unicode rendering of the statement.
        proof:
          type: string
          description: Name of the closing tactic script (`tfe_replay` argument).
          example: tanh_eq_exp; exp_neg; field_simp; ring_nf
        scope:
          type: string
          description: How widely the lemma applies.
          enum:
            - general
            - operator
            - model
        ops:
          type: array
          items:
            type: string
          description: Op Specs the lemma was first proved for (prefetch index).
        nodes:
          type: array
          items:
            type: string
          description: Spec nodes (`<model>:<node path>`) the lemma was proved for.
        source:
          type: string
          description: Where the lemma came from.
          enum:
            - builtin
            - online
            - generalized
        visibility:
          type: string
          description: Library the lemma lives in.
          enum:
            - public
            - org
            - local
        org:
          type: string
          description: >-
            Owning organisation (org library only; never recorded for public
            lemmas).
          nullable: true
        first_solve_ms:
          type: integer
          description: >-
            Solver time of the first proof; used to estimate time saved by a
            hit.
        lean_toolchain:
          type: string
          description: Lean toolchain the proof was checked with.
          example: leanprover/lean4:v4.35.0
        mathlib:
          type: string
          description: Mathlib revision.
          example: v4.35.0
        created:
          type: string
          description: Admission time (ISO 8601).
        hits:
          type: integer
          description: Total hits (Hub-side usage statistics).
        projects:
          type: integer
          description: Number of distinct projects referencing the lemma.
        status:
          type: string
          description: Lifecycle state.
          enum:
            - active
            - pending-migration
            - rejected
        axioms:
          type: array
          items:
            type: string
          description: >-
            Axioms of the compiled theorem (allowlist: propext,
            Classical.choice, Quot.sound).
      required:
        - id
        - statement
        - proof
        - scope
    Error:
      type: object
      properties:
        detail:
          type: string
          description: Why the request was refused.
      required:
        - detail
  securitySchemes:
    bearerAuth:
      type: http
      scheme: bearer
      description: >-
        A Spec Hub API token (`tfe_…`). The CLI reads it from
        `THEFORMALERA_TOKEN` or from `theformalera login`.

````

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