language:en license:cc-by-4.0 arxiv:2311.03755 region:us
---
license: cc-by-4.0
language:
- en
---
# Isa-MMA: Isabelle Components of the Multilingual Mathematical Autoformalization (MMA) Dataset

## Dataset Description
Jiang et. al. published a paper entitled [*Multilingual Mathematical Autoformalization*](https://arxiv.org/abs/2311.03755) that included datasets in Isabelle and Lean. This dataset is the combination of the Isabelle test and Isabelle val datasets merged into one. In addition, this dataset contains formal and informal stastements that have been cleaned of cues. For example, the original datasets had cues within statements for training (e.g.every informal statement ended with "Translate the statement in natural language to Isabelle).
Instead, these have been removed and I have added a text column to match that of the Isa-AF dataset ("Informal statement is: [informal statement value] Formal statement is: [formal statement value]")

## Data Fields
- `input`: The words "Statement in natural language:" followed by a statement in natural language.
- `output`: The statement from the `input` column formalized in Isabelle.