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

# Get a lemma

> One lemma record. Public lemmas never show the contributing organisation.



## OpenAPI

````yaml /api-reference/openapi.json get /v1/lemmas/{lid}
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/{lid}:
    get:
      tags:
        - Lemma Hub
      summary: Get a lemma
      description: >-
        One lemma record. Public lemmas never show the contributing
        organisation.
      operationId: lemma_get_v1_lemmas__lid__get
      parameters:
        - name: lid
          in: path
          required: true
          schema:
            type: string
          description: Lemma id, e.g. `L-d07f2c`.
      responses:
        '200':
          description: OK
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Lemma'
        '404':
          description: No such lemma visible to the caller.
          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.