APRIL: a dataset for learning error correction

Stream: Machine Learning for Theorem Proving

[Vasily Ilin]

I would like to announce our work on error correction in Lean. We built a dataset to learn error correction in Lean without RL, purely with SFT. Check out our paper https://huggingface.co/papers/2602.02990, and the dataset https://huggingface.co/datasets/uw-math-ai/APRIL. This is part of the UW Math AI Lab.
Feedback is very welcome!

[Austin Hatfield]

Oh yay very excited to read!

[Guchan Li]

Interesting! We actually trained Lean provers using compiler feedbacks, and our results are consistent. Although our work's main focus is not the training dataset, it is good to know your work! Our work is currently under ICML2026 review, hope to encounter your work in the future :)