datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
formal-math-autoformalization
Formal Math Autoformalization Dataset
A growing, CC0 public-domain corpus of ⟨natural-language statement ↔ Lean 4 statement + proof⟩ pairs, contributed through the Agentic Commons network.
Why this is scarce data. Mathlib already contains millions of proven Lean theorems — but as bare Lean, with no paired natural language:
theorem add_comm (a b : ℕ) : a + b = b + a := ... -- no "addition on naturals is commutative" attached
The scarce, valuable artifact is the pairing of the… See the full description on the dataset page: https://huggingface.co/datasets/AgenticCommons/formal-math-autoformalization.multilingual-mathematical-autoformalization
Multilingual Mathematical Autoformalization
"Paper"
This repository contains parallel mathematical statements:
Input: An informal proof in natural language
Output: The corresponding formalization in either Lean or Isabelle
This dataset can be used to train models how to formalize mathematical statements into verifiable proofs, a form of machine translation.
Abstract
Autoformalization is the task of translating natural language materials into machine-verifiable… See the full description on the dataset page: https://huggingface.co/datasets/casey-martin/multilingual-mathematical-autoformalization.math_reasoning_autoformalization_track_1AutoformalizationV1_FineTunerepro-formalrx-rectify-and-examine-semantic-failures-in-autoformalization-traces
Agent traces
Agent sessions published from a Trackio Logbook.
math_reasoning_autoformalization_trackDefinition-Autoformalization
Dataset Card for Def_Auto
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.math_reasoning_autoformalization_track_testautoformalization-benchmark-lean4AutoformalizationV1autoformalization-benchautoformalization-clean