@inproceedings{obozov-etal-2025-synthetic, title = "Synthetic Proofs with Tool-Integrated Reasoning: Contrastive Alignment for {LLM} Mathematics with Lean", author = "Obozov, Mark and Diskin, Michael and Beznosikov, Aleksandr and Gasnikov, Alexander and Barannikov, Serguei", editor = "Valentino, Marco and Ferreira, Deborah and Thayaparan, Mokanarangan and Ranaldi, Leonardo and Freitas, Andre", booktitle = "Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025)", month = nov, year = "2025", address = "Suzhou, China", publisher = "Association for Computational Linguistics", url = "https://preview.aclanthology.org/ingest-emnlp/2025.mathnlp-main.15/", pages = "195--202", ISBN = "979-8-89176-348-7" }