The dataset contains both Isabelle and Lean formats, raw dataset from the MMA paper.
Note for Lean portion:
the input always starts with Statement in natural language: as the first line
the output always ends with Translate the statement in natural language to Lean: as the last line.
You may want to remove that before using
