Dataset · Hugging Face

uw-math-ai/APRIL

Name: APRIL
Creator: uw-math-ai
License: apache-2.0
Keywords: task_categories:text-generation, language:en, license:apache-2.0, size_categories:100K<n<1M, arxiv:2602.02990, region:us, lean, formal-verification, theorem-proving, code, math

APRIL Dataset Paper Model & Dataset Download Resource Description Link APRIL Dataset 260K Lean proof-repair tuples with compiler diagnostics and explanations uw-math-ai/APRIL gAPRIL-w-exp Goedel-8B finetuned on APRIL with joint explanation supervision uw-math-ai/gAPRIL-w-exp gAPRIL-wo-exp Goedel-8B finetuned on APRIL for repair only (no explanations) uw-math-ai/gAPRIL-wo-exp Dataset Description The APRIL dataset contains 258,103 examples of… See the full description on the dataset page: https://huggingface.co/datasets/uw-math-ai/APRIL.

View on Hugging FaceReport an issue

Author / organization	uw-math-ai
License (as declared)	apache-2.0
Downloads	628 (as reported by Hugging Face)
Likes	10
Created	2 February 2026
Last updated at source	27 February 2026

leanformal-verificationtheorem-provingcodemath

Embed this entry

<iframe src="https://silytics.si/embed/item/1bbbc8a3-902a-4832-83aa-e5ad763a8ad3" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

More from uw-math-ai

uw-math-ai/math-graphDataset
uw-math-ai/theorem-search-datasetDataset
uw-math-ai/theorem-matchingDataset

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 16 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.