This format corresponds to the proofstep objective from Han et al ICLR 2022.
The python/train directory in the repository shows how the model was fine-tuned.

Please see the repository for more details.

@misc{llmstep,
  author = {Sean Welleck},
  title = {llmstep: LLM proofstep suggestions in Lean},
  year = {2023},
  publisher = {GitHub},
  journal = {GitHub repository},
  howpublished = {\url{https://github.com/wellecks/llmstep}},
}

wellecks/llmstep-mathlib4-pythia2.8b

llmstep: [L]LM proofstep suggestions in Lean

wellecks/
llmstep-mathlib4-pythia2.8b