---
title: "Who cites cvc5: A Versatile and Industrial-Strength SMT Solver"
description: "19 papers of the Elamur Research library cite «cvc5: A Versatile and Industrial-Strength SMT Solver», found in their bibliographies; the most…"
canonical: "https://research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [cvc5: A Versatile and Industrial-Strength SMT…](https://md.research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/) / cited by

# Who cites «cvc5: A Versatile and Industrial-Strength SMT Solver»

19 papers of our library cite it (of the 149,439 whose bibliographies we read) · 7 with a page here, the most cited first · [← back to «cvc5: A Versatile and Industrial-Strength SMT Solver»](https://md.research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/)

1. [**Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving arXiv:2502.07640**Yong Lin, Shange Tang, Bohan Lyu, et al.*2025 · 84 citations*](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/)
2. [**A Survey on Deep Learning for Theorem Proving arXiv:2404.09939**Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.*2024 · 46 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/)
3. [**Magnushammer: A Transformer-Based Approach to Premise Selection arXiv:2303.04488**Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.*2023 · 35 citations*](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/)
4. **[Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://md.research.elamur.ai/free/en/papers/li-2024-autoformalize-mathematical-statements-symbolic-equivalence/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Zenan Li, Yifan Wu, Zhaoyu Li, et al.*2024 · 19 citations*
5. **[Neuro-Symbolic Data Generation for Math Reasoning](https://md.research.elamur.ai/free/en/papers/li-2024-neuro-symbolic-data-generation-math/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Zenan Li, Zhi Zhou, Yuan Yao, et al.*2024 · 14 citations*
6. [**Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning arXiv:2502.13834**Zenan Li, Zhaoyu Li, Wen Tang, et al.*2025 · 11 citations*](https://md.research.elamur.ai/free/en/papers/li-2025-proving-olympiad-inequalities-synergizing-llms/)
7. [**Premise Selection for a Lean Hammer arXiv:2506.07477**Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/)

12 more papers of our library cite it; they have no page here yet.

- [← back to](https://md.research.elamur.ai/free/en/papers/barbosa-2022-cvc5-versatile-industrial-strength-smt/) — cvc5: A Versatile and Industrial-Strength SMT Solver