mathlib-initiative/mathlib-tactics

1---2license: apache-2.03language:4  - en5tags:6  - lean47  - mathlib8  - theorem-proving9  - formal-mathematics10pretty_name: Mathlib Tactics11---12 13# Mathlib Tactics14 15This dataset contains tactic invocations with associated goal states from proofs in [Mathlib](https://github.com/leanprover-community/mathlib4/tree/5ed2965256430c3649e86755f9576b54eca72435), the mathematical library for the Lean 4 theorem prover, extracted with [lean_scout](https://github.com/mathlib-initiative/lean_scout).16 17Extracted from the Mathlib commit with the following hash.18```195ed2965256430c3649e86755f9576b54eca7243520```21 22The dataset follows this schema:23 24```yaml25fields:26- type:27    datatype: string28  nullable: true29  name: module30- type:31    datatype: struct32    children:33    - type:34        datatype: nat35      nullable: false36      name: line37    - type:38        datatype: nat39      nullable: false40      name: column41  nullable: false42  name: startPos43- type:44    datatype: struct45    children:46    - type:47        datatype: nat48      nullable: false49      name: line50    - type:51        datatype: nat52      nullable: false53      name: column54  nullable: false55  name: endPos56- type:57    datatype: struct58    children:59    - type:60        datatype: nat61      nullable: false62      name: line63    - type:64        datatype: nat65      nullable: false66      name: column67  nullable: false68  name: nextStartPos69- type:70    item:71      datatype: struct72      children:73      - type:74          datatype: string75        nullable: false76        name: pp77      - type:78          datatype: string79        nullable: false80        name: ppTerm81      - type:82          datatype: bool83        nullable: false84        name: assigned85      - type:86          item:87            datatype: string88          datatype: list89        nullable: false90        name: usedConstants91      - type:92          item:93            datatype: string94          datatype: list95        nullable: false96        name: usedFVars97      - type:98          item:99            datatype: struct100            children:101            - type:102                datatype: bool103              nullable: false104              name: new105            - type:106                datatype: nat107              nullable: true108              name: index109            - type:110                datatype: string111              nullable: false112              name: kind113            - type:114                datatype: string115              nullable: false116              name: pp117            - type:118                datatype: string119              nullable: false120              name: ppTerm121          datatype: list122        nullable: false123        name: usedGoals124    datatype: list125  nullable: false126  name: goals127- type:128    item:129      datatype: string130    datatype: list131  nullable: false132  name: goalsAfter133- type:134    datatype: string135  nullable: false136  name: ppTac137- type:138    datatype: string139  nullable: false140  name: elaborator141- type:142    datatype: string143  nullable: false144  name: kind145```146 147# Attribution148 149This dataset is derived from [Mathlib](https://github.com/leanprover-community/mathlib4), an open-source mathematical library developed by the [leanprover-community](https://leanprover-community.github.io/). If you use this dataset, please cite the [Mathlib paper](https://doi.org/10.1145/3372885.3373824) or the [Mathlib repository](https://github.com/leanprover-community/mathlib4).150 151A full list of Mathlib contributors is available at: https://github.com/leanprover-community/mathlib4/graphs/contributors152