mathlib-initiative/mathlib-tactics

---
license: apache-2.0
language:
- en
tags:
- lean4
- mathlib
- theorem-proving
- formal-mathematics
pretty_name: Mathlib Tactics
---

# Mathlib Tactics

This dataset contains tactic invocations with associated goal states from proofs in [Mathlib](https://github.com/leanprover-community/mathlib4/tree/5e932f97dd25535344f80f9dd8da3aab83df0fe6), the mathematical library for the Lean 4 theorem prover, extracted with [lean_scout](https://github.com/mathlib-initiative/lean_scout).

Extracted from the Mathlib commit with the following hash.
```
5e932f97dd25535344f80f9dd8da3aab83df0fe6
```

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:
item:
datatype: struct
children:
- type:
datatype: string
nullable: false
name: pp
- type:
item:
datatype: string
datatype: list
nullable: false
name: usedConstants
datatype: list
nullable: false
name: goals
- 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](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).

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