---
title: "Who cites Formalising perfectoid spaces — 9 citing papers"
description: "9 papers of the Elamur Research library cite «Formalising perfectoid spaces», found in their bibliographies; the most cited first."
canonical: "https://research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [Formalising perfectoid spaces](https://md.research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/) / cited by

# Who cites «Formalising perfectoid spaces»

9 papers of our library cite it (of the 149,439 whose bibliographies we read) · 9 with a page here, the most cited first · [← back to «Formalising perfectoid spaces»](https://md.research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/)

1. **[The Lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/) [ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/)**The mathlib Community*2019 · 249 citations*
2. [**The Lean 4 Theorem Prover and Programming Language (System Description) CADE-28 (LNCS 12,699), Springer**Leonardo de Moura, Sebastian Ullrich*2021 · 155 citations*](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
3. [**ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics arXiv:2302.12433**Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, et al.*2023 · 142 citations*](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/)
4. [**Proof Artifact Co-training for Theorem Proving with Language Models arXiv:2102.06203**Jesse Michael Han, Jason Rute, Yuhuai Wu, et al.*2021 · 82 citations*](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/)
5. [**LEGO-Prover: Neural Theorem Proving with Growing Libraries arXiv:2310.00656**Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.*2023 · 79 citations*](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/)
6. [**LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning arXiv:2101.06223**Yuhuai Wu, Markus Rabe, Wenda Li, et al.*2021 · 39 citations*](https://md.research.elamur.ai/free/en/papers/wu-2021-lime-learning-inductive-bias-primitives/)
7. **[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*
8. **[Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers](https://md.research.elamur.ai/free/en/papers/alfarano-2024-global-lyapunov-functions-long-standing/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Alberto Alfarano, François Charton, Amaury Hayat*2024 · 19 citations*
9. [**GFLean: An Autoformalisation Framework for Lean via GF arXiv:2404.01234**Shashank Pathak*2024 · 5 citations*](https://md.research.elamur.ai/free/en/papers/pathak-2024-gflean-autoformalisation-framework-lean-gf/)
- [← back to](https://md.research.elamur.ai/free/en/papers/buzzard-2019-formalising-perfectoid-spaces/) — Formalising perfectoid spaces