Text · dataset · 2026
openbmb/FormalVerse
Listed in Hugging Face Datasets
Description
MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement FormalVerse is a verified Lean 4 autoformalization dataset released with the paper MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement. Every example is produced by the MathForm pipeline, which retrieves relevant Mathlib knowledge before generation and refines each candidate using Lean compiler diagnostics and… See the full description on the dataset page: huggingface.co/datasets/openbmb/FormalVerse.
Links
Where it is published
- Hugging Face dataset page huggingface.co/datasets/openbmb/FormalVerse ↗
landing page · from Hugging Face
Documentation and papers
- arXiv:2608.14221 arxiv.org/abs/2608.14221 ↗
publication · from Hugging Face
Catalogue records · 1
- Hub API huggingface.co/api/datasets/openbmb/FormalVerse ↗
metadata API · from Hugging Face
Topics
- Stated by source
- text · text generation
- From keywords
- Computer Science & AI · Mathematics & Statistics
Provenance · 1 source records, 11 field assertions
| Source | Key | Last seen | Raw |
|---|---|---|---|
| Hugging Face Datasets | openbmb/FormalVerse | 13 d ago | JSON v1 |
| Field | Assertion | Extractor | Evidence |
|---|---|---|---|
| access_level | source · Hugging Face | connector:huggingface@1.0.0 | /gated |
| concepts[field].local:field:computer-science-ai | mapping · Hugging Face | connector:huggingface@1.0.0 | |
| concepts[field].local:field:mathematics-statistics | mapping · Hugging Face | vocabulary-mapper@1.0.0 | keywords['mathematics'] |
| concepts[modality].hf_modality:text | source · Hugging Face | connector:huggingface@1.0.0 | |
| concepts[task].hf_task:text-generation | source · Hugging Face | connector:huggingface@1.0.0 | /tags[task_categories:*] |
| created_date | source · Hugging Face | connector:huggingface@1.0.0 | |
| description | source · Hugging Face | connector:huggingface@1.0.0 | /description |
| license | source · Hugging Face | connector:huggingface@1.0.0 | /tags[license:*] |
| publication_date | source · Hugging Face | connector:huggingface@1.0.0 | |
| title | source · Hugging Face | connector:huggingface@1.0.0 | /id |
| updated_date | source · Hugging Face | connector:huggingface@1.0.0 |