Lean-ByT5 is a ByT5-small model fine-tuned on the augmented Lean-Mathlib data for Lean theorem proving.

The model performs sequence-to-sequence generation, generating Lean tactics for a given statement goal.

For more details on the training methodology, data augmentation strategy, and dynamic sampling method used for Lean theorem proving, please refer to our paper:

Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
Rahul Vishwakarma, Subhankar Mishra
arXiv:2312.14188 (cs.AI, cs.LG, cs.LO)

Paper: https://arxiv.org/abs/2312.14188

If you use this model or build upon this work, please cite: