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

# Search lemmas

> Search the public library (and the caller's org library with a token) by statement text, Op Spec or node. At most 200 results.



## OpenAPI

````yaml /api-reference/openapi.json get /v1/lemmas
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:
    get:
      tags:
        - Lemma Hub
      summary: Search lemmas
      description: >-
        Search the public library (and the caller's org library with a token) by
        statement text, Op Spec or node. At most 200 results.
      operationId: lemma_search_v1_lemmas_get
      parameters:
        - name: q
          in: query
          required: false
          schema:
            type: string
            default: ''
          description: Text contained in the statement or id.
        - name: op
          in: query
          required: false
          schema:
            type: string
          description: Op Spec name, e.g. `TheFormalEra.Ops.siluMul`.
        - name: node
          in: query
          required: false
          schema:
            type: string
          description: Node path suffix, e.g. `mlp.act`.
      responses:
        '200':
          description: OK
          content:
            application/json:
              schema:
                type: object
                properties:
                  lemmas:
                    type: array
                    items:
                      $ref: '#/components/schemas/Lemma'
                    description: Matching lemmas.
        '422':
          description: Validation error
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/HTTPValidationError'
      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
    HTTPValidationError:
      properties:
        detail:
          items:
            $ref: '#/components/schemas/ValidationError'
          type: array
          title: Detail
      type: object
      title: HTTPValidationError
    ValidationError:
      properties:
        loc:
          items:
            anyOf:
              - type: string
              - type: integer
          type: array
          title: Location
        msg:
          type: string
          title: Message
        type:
          type: string
          title: Error Type
        input:
          title: Input
        ctx:
          type: object
          title: Context
      type: object
      required:
        - loc
        - msg
        - type
      title: ValidationError
  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.