---
license: apache-2.0
language:
- en
base_model:
- google/byt5-small
tags:
- theorem-proving
- lean
- byt5
- mathematics
- code
---

# Lean-ByT5
**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.

## Base Model
- google/byt5-small (Apache License 2.0)

## Training
- PyTorch Lightning

## Related Paper & Citation
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:
```bibtex
@article{vishwakarma2023enhancing,
  title={Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method},
  author={Vishwakarma, Rahul and Mishra, Subhankar},
  journal={arXiv preprint arXiv:2312.14188},
  year={2023},
  primaryClass={cs.AI}
}