HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

Yang Li, Dong Du, Linfeng Song +4

We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a…