Datasetpublic

mathlib-initiative/mathlib-tactics

Mathlib Tactics This dataset contains tactic invocations with associated goal states from proofs in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout. Extracted from the Mathlib commit with the following hash. d13f23b723b8a846827a245b89c10fc7d3f11612 The dataset follows this schema: fields: - type: datatype: string nullable: true name: module - type: datatype: struct children: - type: datatype: nat… See the full description on the dataset page: https://huggingface.co/datasets/mathlib-initiative/mathlib-tactics.

sourceHugging Faceapache-2.0updated 10d agoView on Hugging Face

2likes1.9kdownloads

Dataset Card

Mathlib Tactics

This dataset contains tactic invocations with associated goal states from proofs in Mathlib, the mathematical library for the Lean 4 theorem prover, extracted with lean_scout.

Extracted from the Mathlib commit with the following hash.

d13f23b723b8a846827a245b89c10fc7d3f11612

The dataset follows this schema:

yaml

fields:
- type:
    datatype: string
  nullable: true
  name: module
- type:
    datatype: struct
    children:
    - type:
        datatype: nat
      nullable: false
      name: line
    - type:
        datatype: nat
      nullable: false
      name: column
  nullable: false
  name: startPos
- type:
    datatype: struct
    children:
    - type:
        datatype: nat
      nullable: false
      name: line
    - type:
        datatype: nat
      nullable: false
      name: column
  nullable: false
  name: endPos
- type:
    datatype: struct
    children:
    - type:
        datatype: nat
      nullable: false
      name: line
    - type:
        datatype: nat
      nullable: false
      name: column
  nullable: false
  name: nextStartPos
- type:
    item:
      datatype: struct
      children:
      - type:
          datatype: string
        nullable: false
        name: pp
      - type:
          datatype: string
        nullable: false
        name: ppTerm
      - type:
          datatype: bool
        nullable: false
        name: assigned
      - type:
          item:
            datatype: string
          datatype: list
        nullable: false
        name: usedConstants
      - type:
          item:
            datatype: string
          datatype: list
        nullable: false
        name: usedFVars
      - type:
          item:
            datatype: struct
            children:
            - type:
                datatype: bool
              nullable: false
              name: new
            - type:
                datatype: nat
              nullable: true
              name: index
            - type:
                datatype: string
              nullable: false
              name: kind
            - type:
                datatype: string
              nullable: false
              name: pp
            - type:
                datatype: string
              nullable: false
              name: ppTerm
          datatype: list
        nullable: false
        name: usedGoals
    datatype: list
  nullable: false
  name: goals
- type:
    item:
      datatype: string
    datatype: list
  nullable: false
  name: goalsAfter
- type:
    datatype: string
  nullable: false
  name: ppTac
- type:
    datatype: string
  nullable: false
  name: elaborator
- type:
    datatype: string
  nullable: false
  name: kind

Attribution

This dataset is derived from Mathlib, an open-source mathematical library developed by the leanprover-community. If you use this dataset, please cite the Mathlib paper or the Mathlib repository.

A full list of Mathlib contributors is available at: https://github.com/leanprover-community/mathlib4/graphs/contributors