Model Card: Assisting Mathematical Formalization with A Learning-based Premise Retriever

Model Description

This model is the first version designed for premise retrieval in Lean, based on the state representation of Lean. The model follows the architecture described in the paper:

Assisting Mathematical Formalization with A Learning-based Premise Retriever

The model implementation and code are available at:

GitHub Repository

Try our model

Citation

If you use this model, please cite the following paper:

@misc{tao2025assistingmathematicalformalizationlearningbased,
      title={Assisting Mathematical Formalization with A Learning-based Premise Retriever}, 
      author={Yicheng Tao and Haotian Liu and Shanwen Wang and Hongteng Xu},
      year={2025},
      eprint={2501.13959},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2501.13959}, 
}