--- title: "Who cites Exploration of Neural Machine — 32 citing papers" description: "32 papers of the Elamur Research library cite «Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar»…" canonical: "https://research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/cited-by/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/cited-by/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [Exploration of Neural Machine Translation in…](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/) / cited by # Who cites «Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar» 32 papers of our library cite it (of the 149,439 whose bibliographies we read) · 20 with a page here, the most cited first · [← back to «Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar»](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/) 1. [**Autoformalization with Large Language Models arXiv:2205.12615**Yuhuai Wu, Albert Q. Jiang, Wenda Li, et al.*2022 · 204 citations*](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/) 2. [**Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs arXiv:2210.12283**Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, et al.*2022 · 178 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/) 3. **[LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://md.research.elamur.ai/free/en/papers/olausson-2023-linc-neurosymbolic-approach-logical-reasoning/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Theo X. Olausson, Alex Gu, Benjamin Lipkin, et al.*2023 · 172 citations* 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. [**NaturalProofs: Mathematical Theorem Proving in Natural Language arXiv:2104.01112**Sean Welleck, Jiacheng Liu, Ronan Le Bras, et al.*2021 · 76 citations*](https://md.research.elamur.ai/free/en/papers/welleck-2021-naturalproofs-mathematical-theorem-proving-natural/) 6. **[NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://md.research.elamur.ai/free/en/papers/welleck-2022-naturalprover-grounded-mathematical-proof-generation/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Sean Welleck, Jiacheng Liu, Ximing Lu, et al.*2022 · 62 citations* 7. [**Mathematical Reasoning via Self-supervised Skip-tree Training arXiv:2006.04757**Markus N. Rabe, Dennis Lee, Kshitij Bansal, et al.*2020 · 54 citations*](https://md.research.elamur.ai/free/en/papers/rabe-2020-mathematical-reasoning-self-supervised-skip/) 8. [**Lean-STaR: Learning to Interleave Thinking and Proving arXiv:2407.10040**Haohan Lin, Zhiqing Sun, Sean Welleck, et al.*2024 · 51 citations*](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/) 9. [**Formal Mathematical Reasoning: A New Frontier in AI arXiv:2412.16075**Kaiyu Yang, Gabriel Poesia, Jingxuan He, et al.*2024 · 49 citations*](https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/) 10. [**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/) 11. [**Don't Trust: Verify — Grounding LLM Quantitative Reasoning with Autoformalization arXiv:2403.18120**Jin Peng Zhou, Charles Staats, Wenda Li, et al.*2024 · 45 citations*](https://md.research.elamur.ai/free/en/papers/zhou-2024-don-t-trust-verify-grounding/) 12. [**IsarStep: a Benchmark for High-level Mathematical Reasoning arXiv:2006.09265**Wenda Li, Lei Yu, Yuhuai Wu, et al.*2020 · 43 citations*](https://md.research.elamur.ai/free/en/papers/li-2020-isarstep-benchmark-high-level-mathematical/) 13. **[First Neural Conjecturing Datasets and Experiments](https://md.research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/) [Lecture notes in computer science](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/)**Josef Urban, Jan Jakubův*2020 · 40 citations* 14. [**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/) 15. [**Multilingual Mathematical Autoformalization arXiv:2311.03755**Albert Q. Jiang, Wenda Li, Mateja Jamnik*2023 · 37 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2023-multilingual-mathematical-autoformalization/) 16. [**Process-Driven Autoformalization in Lean 4 arXiv:2406.01940**Jianqiao Lu, Yingjia Wan, Zhengying Liu, et al.*2024 · 33 citations*](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/) 17. [**Lyra: Orchestrating Dual Correction in Automated Theorem Proving arXiv:2309.15806**Chuanyang Zheng, Haiming Wang, Enze Xie, et al.*2023 · 24 citations*](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/) 18. [**Towards a Mathematics Formalisation Assistant using Large Language Models arXiv:2211.07524**Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, et al.*2022 · 19 citations*](https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/) 19. **[ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, et al.*2025 · 16 citations* 20. [**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/) 12 more papers of our library cite it; they have no page here yet. - [← back to](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/) — Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar