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. 5ed2965256430c3649e86755f9576b54eca72435 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.