This dataset is a collection of mathematical definitions designed for evaluating LLMs on autoformalization in the real-world setting.
Dataset Details
Dataset Description
Autoformalization refers to the task of translating mathematical statements written in natural language and LaTeX symbols to a formal language.
The majority of mathematical knowledge is not formalized. Autoformalization could support mathematical discovery and… See the full description on the dataset page: https://huggingface.co/datasets/lanzhang128/Definition-Autoformalization.
