---
title: "Who cites Isabelle: The Next 700 Theorem — 6 citing papers"
description: "6 papers of the Elamur Research library cite «Isabelle: The Next 700 Theorem Provers», found in their bibliographies; the most cited first."
canonical: "https://research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [Isabelle: The Next 700 Theorem Provers](https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/) / cited by

# Who cites «Isabelle: The Next 700 Theorem Provers»

6 papers of our library cite it (of the 149,439 whose bibliographies we read) · 5 with a page here, the most cited first · [← back to «Isabelle: The Next 700 Theorem Provers»](https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/)

1. [**InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning arXiv:2402.06332**Huaiyuan Ying, Shuo Zhang, Linyang Li, et al.*2024 · 90 citations*](https://md.research.elamur.ai/free/en/papers/ying-2024-internlm-math-open-math-large/)
2. **[Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Huaiyuan Ying, Zijian Wu, Yihan Geng, et al.*2024 · 80 citations*
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. [**Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving arXiv:2305.16366**Xueliang Zhao, Wenda Li, Lingpeng Kong*2023 · 29 citations*](https://md.research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/)
5. **[Consistent Autoformalization for Constructing Mathematical Libraries](https://md.research.elamur.ai/free/en/papers/zhang-2024-consistent-autoformalization-constructing-mathematical-libraries/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Lan Zhang, Xin Quan, Andre Freitas*2024 · 11 citations*

1 more paper of our library cites it; it has no page here yet.

- [← back to](https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/) — Isabelle: The Next 700 Theorem Provers