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

# Prefetch lemmas

> Lemmas for the Op Specs of a verification, plus the general ones, from the requested libraries. Only op names and Spec Keys are sent. Without a token only the public library is searched. Results are capped (default 256, max 512) and ranked by hit count; lemmas pending migration are skipped.



## OpenAPI

````yaml /api-reference/openapi.json post /v1/lemmas/prefetch
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/prefetch:
    post:
      tags:
        - Lemma Hub
      summary: Prefetch lemmas
      description: >-
        Lemmas for the Op Specs of a verification, plus the general ones, from
        the requested libraries. Only op names and Spec Keys are sent. Without a
        token only the public library is searched. Results are capped (default
        256, max 512) and ranked by hit count; lemmas pending migration are
        skipped.
      operationId: lemma_prefetch_v1_lemmas_prefetch_post
      parameters: []
      requestBody:
        required: true
        content:
          application/json:
            schema:
              type: object
              properties:
                ops:
                  type: array
                  items:
                    type: string
                  description: Op Spec names (max 200).
                nodes:
                  type: array
                  items:
                    type: string
                  description: Spec Keys of the involved nodes.
                use:
                  type: array
                  items:
                    type: string
                    enum:
                      - public
                      - org
                  description: Libraries to search.
                snapshot:
                  type: string
                  description: '`latest` or an ISO time; lemmas created later are excluded.'
                limit:
                  type: integer
                  description: Maximum records (≤ 512).
            example:
              ops:
                - TheFormalEra.Ops.siluMul
              nodes:
                - Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act
              use:
                - public
                - org
              snapshot: latest
              limit: 256
      responses:
        '200':
          description: OK
          content:
            application/json:
              schema:
                type: object
                properties:
                  records:
                    type: array
                    items:
                      $ref: '#/components/schemas/Lemma'
                    description: Retrieved lemmas.
                  snapshot:
                    type: string
                    description: Snapshot the retrieval corresponds to.
                  org_cap:
                    type: string
                    description: Organisation contribution cap.
                    nullable: true
                  org:
                    type: string
                    description: Caller's organisation.
                    nullable: true
                  plan:
                    type: string
                    description: Caller's plan.
      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
  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.