Elamur Research⌕
☰
home / papers / 2025 / ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data

ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data

Paper · 2025 · Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang et al.

Summary

The paper addresses autoformalization: converting natural-language theorem statements into machine-checkable Lean 4 code. Progress is limited by the scarcity of paired informal–formal data. Existing pipelines either derive data from Mathlib, which caps dataset size, or translate web-scraped problems, which requires heavy filtering. ATLAS takes a different route. It first builds a repository of mathematical concepts drawn from Mathlib ("Data Lifting"). An LLM then writes new natural-language statements that combine these concepts. In the "Data Synthesis" step, a student model formalizes them, while a teacher model (DeepSeek-V3) and the Lean compiler check and repair the output. Two augmentation strategies use Lean's Infoview to derive extra statement pairs, one from proof steps and one from contraposition. The authors repeat the loop for 10 rounds of expert iteration and obtain a 117k-pair undergraduate-level corpus. On this corpus they train the ATLAS Translator, built on Llama3.1-8B-Instruct with LoRA. They report statistically significant gains over Herald Translator and Kimina-Autoformalizer without any human intervention. This shows that scalable, preprocessing-free synthetic data can push formal-math tooling forward.

Key points

  • Resources: the ATLAS dataset contains 117k parallel statements. The MathQual benchmark contains 465 graduate-level natural-language statements. Code, data and model are released on GitHub (XiaoyangLiu-sjtu/ATLAS).
  • On ProofNet, the ATLAS Translator reaches 39.46% pass@1. Its teacher DeepSeek-V3 scores 18.82% and the initialization model scores 23.56%.
  • ATLAS uses about 117k training examples. Herald Translator uses roughly 1,160k, and Kimina-Autoformalizer relied on Lean 4 experts during training.
  • Full-parameter fine-tuning beats LoRA for all three base models tested. DeepSeek-Prover-V1.5-7B-Base performs best, with pass@1 of 77.25% on miniF2F, 54.99% on ProofNet and 42.49% on PutnamBench.
  • In the ablation study, dropping the synthetic data hurts performance most. Removing the proof-based or contraposition-based augmentation causes smaller declines.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Shanghai Jiao Tong UniversityShanghai · China149 works · 16,161 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 worksComputational Theory and Mathematics · 252 works

Cite

Cite as Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao and Tao Luo. 2025. ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data. arXiv:2502.05567.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2502.05567 · arXiv 2502.05567

@misc{liu2025atlas,
  title = {{ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data}},
  author = {Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao and Tao Luo},
  year = {2025},
  doi = {10.48550/arxiv.2502.05567},
  eprint = {2502.05567},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2502.05567}
}

References

58 references, 21 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. A. Agrawal, S. Gadgil, N. Goyal, A. Narayanan, and A. Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524, 2022. find
  2. Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  3. Z. Azerbayev, H. Schoelkopf, K. Paster, M. D. Santos, S. McAleer, A. Q. Jiang, J. Deng, S. Biderman, and S. Welleck. Llemma: An open language model for mathematics. In The Twelfth International Conference on Learning Representations, 2024.
  4. B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliâtre, E. Giménez, H. Herbelin, et al. The Coq proof assistant reference manual. INRIA, version, 6(11), 1999. find
  5. M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. D. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021.
  6. G. Cunningham, R. C. Bunescu, and D. Juedes. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. In Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP), pages 25–32. Association for Computational Linguistics, 2023. find
  7. L. De Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer, 2015. find
  8. A. Dubey, A. Jauhri, A. Pandey, A. Kadian, A. Al-Dahle, A. Letman, A. Mathur, A. Schelten, A. Yang, A. Fan, et al. The Llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024.
  9. G. Gao, Y. Wang, J. Jiang, Q. Gao, Z. Qin, T. Xu, and B. Dong. Herald: A natural language annotated Lean 4 dataset. In The Thirteenth International Conference on Learning Representations, 2024. find
  10. J. Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996. find
  11. G. Hinton, O. Vinyals, and J. Dean. Distilling the knowledge in a neural network. arXiv preprint arXiv:1503.02531, 2015.
  12. A. Holtzman, J. Buys, L. Du, M. Forbes, and Y. Choi. The curious case of neural text degeneration. In International Conference on Learning Representations, 2020.
  13. E. J. Hu, yelong shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang, L. Wang, and W. Chen. LoRA: Low-rank adaptation of large language models. In International Conference on Learning Representations, 2022.
  14. Y. Huang, X. Lin, Z. Liu, Q. Cao, H. Xin, H. Wang, Z. Li, L. Song, and X. Liang. MUSTARD: Mastering uniform synthesis of theorem and proof data. In The Twelfth International Conference on Learning Representations, 2024. find
  15. A. Q. Jiang, W. Li, and M. Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023. find
  16. A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023.
  17. A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y. Wu. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023.
  18. J. Li, E. Beeching, L. Tunstall, B. Lipkin, R. Soletskyi, S. Huang, K. Rasul, L. Yu, A. Q. Jiang, Z. Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13:9, 2024. find
  19. Y. Li, D. Du, L. Song, C. Li, W. Wang, T. Yang, and H. Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024.
  20. Z. Li, Y. Wu, Z. Li, X. Wei, X. Zhang, F. Yang, and X. Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. find
  21. Y. Lin, S. Tang, B. Lyu, J. Wu, H. Lin, K. Yang, J. Li, M. Xia, D. Chen, S. Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025. find
  22. A. Liu, B. Feng, B. Wang, B. Wang, B. Liu, C. Zhao, C. Dengr, C. Ruan, D. Dai, D. Guo, et al. Deepseek-v2: A strong, economical, and efficient mixture-of-experts language model. arXiv preprint arXiv:2405.04434, 2024. find
  23. A. Liu, B. Feng, B. Xue, B. Wang, B. Wu, C. Lu, C. Zhao, C. Deng, C. Zhang, C. Ruan, et al. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437, 2024. find
  24. Q. Liu, X. Zheng, X. Lu, Q. Cao, and J. Yan. Rethinking and improving autoformalization: Towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025. find
  25. J. Lu, Y. Wan, Y. Huang, J. Xiong, Z. Liu, and Z. Guo. Formalalign: Automated alignment evaluation for autoformalization. In The Thirteenth International Conference on Learning Representations, 2024.
  26. J. Lu, Y. Wan, Z. Liu, Y. Huang, J. Xiong, C. Liu, J. Shen, H. Jin, J. Zhang, H. Wang, et al. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406.01940, 2024. find
  27. L. d. Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021.
  28. L. Murphy, K. Yang, J. Sun, Z. Li, A. Anandkumar, and X. Si. Autoformalizing euclidean geometry. In Forty-first International Conference on Machine Learning, 2024. find
  29. L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. find
  30. S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  31. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  32. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
  33. V. Shah, D. Yu, K. Lyu, S. Park, N. R. Ke, M. C. Mozer, Y. Bengio, S. Arora, and A. Goyal. AI-assisted generation of difficult math questions. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. find
  34. C. Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pages 3–20. Springer, 2020. find
  35. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, Jan. 2020. find
  36. G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. find
  37. H. Wang, M. Unsal, X. Lin, M. Baksys, J. Liu, M. D. Santos, F. Sung, M. Vinyes, Z. Ying, Z. Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025. find
  38. H. Wang, H. Xin, C. Zheng, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin, Z. Li, and X. Liang. LEGO-Prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024. find
  39. Q. Wang, C. Brown, C. Kaliszyk, and J. Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 85–98, 2020. find
  40. Q. Wang, C. Kaliszyk, and J. Urban. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pages 255–270. Springer, 2018. find
  41. R. Wang, J. Zhang, Y. Jia, R. Pan, S. Diao, R. Pi, and T. Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024. find
  42. X. Wang, Y. Chen, and W. Zhu. A survey on curriculum learning. IEEE transactions on pattern analysis and machine intelligence, 44(9):4555–4576, 2021. find
  43. Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353– 32368, 2022.
  44. Z. Wu, S. Huang, Z. Zhou, H. Ying, J. Wang, D. Lin, and K. Chen. Internlm2.5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024. find
  45. Z. Wu, J. Wang, D. Lin, and K. Chen. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227, 2024. find
  46. H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. DeepSeek-Prover: Advancing theorem proving in llms through large-scale synthetic data. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024.
  47. H. Xin, Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, W. Gao, H. Zhang, Q. Zhu, D. Yang, Z. Gou, Z. Wu, F. Luo, and C. Ruan. DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. In The Thirteenth International…
  48. R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y. Sun, S. Zheng, and K. Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025. find
  49. A. Yang, B. Yang, B. Zhang, B. Hui, B. Zheng, B. Yu, C. Li, D. Liu, F. Huang, H. Wei, et al. Qwen2.5 technical report. arXiv preprint arXiv:2412.15115, 2024. find
  50. K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. J. Prenger, and A. Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024.
  51. H. Ying, Z. Wu, Y. Geng, J. Wang, D. Lin, and K. Chen. Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. find
  52. H. Ying, S. Zhang, L. Li, Z. Zhou, Y. Shao, Z. Fei, Y. Ma, J. Hong, K. Liu, Z. Wang, Y. Wang, Z. Wu, S. Li, F. Zhou, H. Liu, S. Zhang, W. Zhang, H. Yan, X. Qiu, J. Wang, K. Chen, and D. Lin. InternLM-Math: Open math large language models toward verifiable reasoning. CoRR, abs/2402.06332, 2024. find
  53. L. Yujian and L. Bo. A normalized levenshtein distance metric. IEEE transactions on pattern analysis and machine intelligence, 29(6):1091–1095, 2007. find
  54. L. Zhang, X. Quan, and A. Freitas. Consistent autoformalization for constructing mathematical libraries. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020–4033. Association for Computational Linguistics, Nov. 2024. find
  55. C. Zheng, H. Wang, E. Xie, Z. Liu, J. Sun, H. Xin, J. Shen, Z. Li, and Y. Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806, 2023. find
  56. K. Zheng, J. M. Han, and S. Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations, 2022.
  57. Y. Zheng, R. Zhang, J. Zhang, Y. Ye, and Z. Luo. LlamaFactory: Unified efficient fine-tuning of 100+ language models. In Y. Cao, Y. Feng, and D. Xiong, editors, Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations), pages 400–410. A…
  58. J. P. Zhou, C. E. Staats, W. Li, C. Szegedy, K. Q. Weinberger, and Y. Wu. Don’t Trust: Verify – grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, 2024. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/