---
title: "A Semantic Search Engine for Mathlib4 — Gao 2024"
description: "Finding a needed theorem in mathlib4, the Lean 4 mathematical library, is hard for anyone who… 41 references, cited by 11 papers here."
authors: ["Guoxiong Gao", "Haocheng Ju", "Jiedong Jiang", "Zihan Qin", "Bin Dong"]
year: 2024
venue: "Findings of the Association for Computational Linguistics: EMNLP 2024"
source: "https://aclanthology.org/2024.findings-emnlp.470/"
doi: "10.18653/v1/2024.findings-emnlp.470"
arxiv: "2403.13310"
licence: "CC BY 4.0 (ACL Anthology)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/gao-2024-semantic-search-engine-mathlib4/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/gao-2024-semantic-search-engine-mathlib4/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/9/) / A Semantic Search Engine for Mathlib4

# A Semantic Search Engine for Mathlib4

**Authors:** [Guoxiong Gao](https://md.research.elamur.ai/free/en/authors/guoxiong-gao/), [Haocheng Ju](https://md.research.elamur.ai/free/en/authors/haocheng-ju/), [Jiedong Jiang](https://md.research.elamur.ai/free/en/authors/jiedong-jiang/), Zihan Qin and [Bin Dong](https://md.research.elamur.ai/free/en/authors/bin-dong/) · **Year:** 2024 · **Venue:** [Findings of the Association for Computational Linguistics: EMNLP 2024](https://md.research.elamur.ai/free/en/venues/findings/) ([Findings of the Association for Computational Linguistics 2024](https://md.research.elamur.ai/free/en/venues/findings/2024/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://aclanthology.org/2024.findings-emnlp.470/) · [PDF](https://aclanthology.org/2024.findings-emnlp.470.pdf) · [DOI 10.18653/v1/2024.findings-emnlp.470](https://doi.org/10.18653/v1/2024.findings-emnlp.470) · [arXiv 2403.13310](https://arxiv.org/abs/2403.13310) · [OpenAlex](https://openalex.org/W4404781986)

**Citations:** 3 citations (OpenAlex, 2026-10-14) · [11](https://md.research.elamur.ai/free/en/papers/gao-2024-semantic-search-engine-mathlib4/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Finding a needed theorem in mathlib4, the Lean 4 mathematical library, is hard for anyone who doesn't know its naming conventions. The official documentation search matches formal names, and GitHub keyword search depends on docstrings that many theorems lack. The authors built a semantic search engine, LeanSearch, that takes informal natural-language queries.

They first "informalize" mathlib4. An LLM receives each theorem's name, formal statement, docstring and the definitions linked from it, and returns an informal name and statement. The resulting informal–formal pairs are embedded and stored in a vector database. Incoming queries are augmented with an LLM before dense retrieval. The authors also built a benchmark of queries for comparing mathlib4 search tools, including Moogle.

The best setup used the E5 mistral-7b embedding model over the combined formal+informal corpus with query augmentation. It beat purely formal or purely informal corpora and the OpenAI v3 large embeddings. The tool and its data are publicly released and lower the entry barrier for formalizing mathematics in Lean.

## Key points
- The informalizer is gpt-3.5-turbo-16k at temperature 0. Its prompt includes linked definitions and docstrings, which is richer context than the formal-only approach of Jiang et al. (2023).
- The best reported configuration reached an averaged nDCG@20 of about 0.733 and an R@10 of about 0.913 (Table 5). Without query augmentation, the same configuration still averaged about 0.701.
- Query augmentation improved every method tested, especially on the Theorem Names query group. On the Lean 4 Terms group, adding informal text tended to hurt, because those queries depend on lexical matching.
- The engine is live at leansearch.net, and the code and data are at github.com/reaslab/LeanSearch.
- The authors list two limitations. Hyperlink-based dependency extraction can miss definitions, and the 7B embedding model is heavy for low-resource devices.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Peking University](https://md.research.elamur.ai/free/en/universities/peking-university/) — University, Beijing, China · 244 works · 39,359 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works · [🗄️ Information Systems](https://md.research.elamur.ai/free/en/shelves/computer-science/information-systems/) · 1,437 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 252 works

🧭 Topics (2): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,426 works · [🔍 Information retrieval & search](https://md.research.elamur.ai/free/en/topics/information-retrieval/) · 473 works

💡 Concepts (1): [💡 Inverted index](https://md.research.elamur.ai/free/en/concepts/inverted-index/) · 26 works

## Cite

Cite as: Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin and Bin Dong. 2024. A Semantic Search Engine for Mathlib4. Findings of the Association for Computational Linguistics: EMNLP 2024.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{gao2024semantic,
  title = {{A Semantic Search Engine for Mathlib4}},
  author = {Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin and Bin Dong},
  booktitle = {Findings of the Association for Computational Linguistics: EMNLP 2024},
  year = {2024},
  doi = {10.18653/v1/2024.findings-emnlp.470},
  eprint = {2403.13310},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2024.findings-emnlp.470}
}
```

- [← previous When "Competency" in Reasoning Opens the Door to Vulnerability: Jailbreaking LLMs via Novel Complex Ciphers](https://md.research.elamur.ai/free/en/papers/handa-2024-competency-reasoning-opens-door-vulnerability/)
- [next → Alignment at Pre-training! Towards Native Alignment for Arabic LLMs](https://md.research.elamur.ai/free/en/papers/liang-2024-alignment-pre-training-towards-native/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/9/)

## References

41 references, 14 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Wei-Cheng Chang, Felix X. Yu, Yin-Wen Chang, Yiming Yang, and Sanjiv Kumar. 2020. Pre-training Tasks for Embedding-based Large-scale Retrieval. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net. [find](https://scholar.google.com/scholar?q=Wei%2DCheng+Chang%2C+Felix+X%2E+Yu%2C+Yin%2DWen+Chang%2C+Yiming+Yang%2C+and+Sanjiv+Kumar%2E+2020%2E+Pre%2Dtraining+Tasks+for+Embedding%2Dbased+Large%2Dscale+Retrieval%2E+In+8th+International+Conference+on+Learning+Representati)
2. Leonardo de Moura and Sebastian Ullrich. 2021. [The Lean 4 Theorem Prover and Programming Language](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/). In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625– 635.…
3. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of… [find](https://scholar.google.com/scholar?q=Leonardo+Mendon%C3%A7a+de+Moura%2C+Soonho+Kong%2C+Jeremy+Avigad%2C+Floris+van+Doorn%2C+and+Jakob+von+Raumer%2E+2015%2E+The+Lean+Theorem+Prover+%28System+Description%29%2E+In+Automated+Deduction+%2D+CADE%2D25+%2D+25th+Internationa)
4. Dallas Fraser, Andrew Kane, and Frank Wm. Tompa. 2018. Choosing Math Features for BM25 Ranking with Tangent-L. In Proceedings of the ACM Symposium on Document Engineering 2018, DocEng ’18, New York, NY, USA. Association for Computing Machinery. [find](https://scholar.google.com/scholar?q=Dallas+Fraser%2C+Andrew+Kane%2C+and+Frank+Wm%2E+Tompa%2E+2018%2E+Choosing+Math+Features+for+BM25+Ranking+with+Tangent%2DL%2E+In+Proceedings+of+the+ACM+Symposium+on+Document+Engineering+2018%2C+DocEng+%E2%80%9918%2C+New+York%2C+N)
5. Liangcai Gao, Ke Yuan, Yuehan Wang, Zhuoren Jiang, and Zhi Tang. 2016. The Math Retrieval System of ICST for NTCIR-12 MathIR Task. In Proceedings of the 12th NTCIR Conference on Evaluation of Information Access Technologies, National Center of Sciences, Tokyo, Japan, June 7-10, 2016. National Instit… [find](https://scholar.google.com/scholar?q=Liangcai+Gao%2C+Ke+Yuan%2C+Yuehan+Wang%2C+Zhuoren+Jiang%2C+and+Zhi+Tang%2E+2016%2E+The+Math+Retrieval+System+of+ICST+for+NTCIR%2D12+MathIR+Task%2E+In+Proceedings+of+the+12th+NTCIR+Conference+on+Evaluation+of+Informat)
6. Po-Sen Huang, Xiaodong He, Jianfeng Gao, Li Deng, Alex Acero, and Larry Heck. 2013. Learning deep structured semantic models for web search using clickthrough data. In Proceedings of the 22nd ACM International Conference on Information & Knowledge Management, CIKM ’13, page 2333–2338, New York, NY,… [find](https://scholar.google.com/scholar?q=Po%2DSen+Huang%2C+Xiaodong+He%2C+Jianfeng+Gao%2C+Li+Deng%2C+Alex+Acero%2C+and+Larry+Heck%2E+2013%2E+Learning+deep+structured+semantic+models+for+web+search+using+clickthrough+data%2E+In+Proceedings+of+the+22nd+ACM+Inte)
7. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. 2023. Multilingual Mathematical Autoformalization. CoRR, abs/2311.03755. [find](https://scholar.google.com/scholar?q=Albert+Q%2E+Jiang%2C+Wenda+Li%2C+and+Mateja+Jamnik%2E+2023%2E+Multilingual+Mathematical+Autoformalization%2E+CoRR%2C+abs%2F2311%2E03755%2E)
8. Andrew Kane, Yin Ki Ng, and Frank Wm. Tompa. 2022. Dowsing for Answers to Math Questions: Doing Better with Less. In Proceedings of the Working Notes of CLEF 2022 - Conference and Labs of the Evaluation Forum, Bologna, Italy, September 5th -to - 8th, 2022, volume 3180 of CEUR Workshop Proceedings, p… [find](https://scholar.google.com/scholar?q=Andrew+Kane%2C+Yin+Ki+Ng%2C+and+Frank+Wm%2E+Tompa%2E+2022%2E+Dowsing+for+Answers+to+Math+Questions%3A+Doing+Better+with+Less%2E+In+Proceedings+of+the+Working+Notes+of+CLEF+2022+%2D+Conference+and+Labs+of+the+Evaluati)
9. Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. 2020. [Dense Passage Retrieval for Open-Domain Question Answering](https://md.research.elamur.ai/free/en/papers/karpukhin-2020-dense-passage-retrieval-open-domain/). In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 6769– 6781, Onl…
10. Omar Khattab and Matei Zaharia. 2020. [ColBERT: Efficient and Effective Passage Search via Contextualized Late Interaction over BERT](https://md.research.elamur.ai/free/en/papers/khattab-2020-colbert-efficient-effective-passage/). In Proceedings of the 43rd International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’20, page 39–48, New York, NY, USA. Associati…
11. Giovanni Yoko Kristianto, Goran Topic, and Akiko Aizawa. 2016. MCAT Math Retrieval System for NTCIR-12 MathIR Task. In Proceedings of the 12th NTCIR Conference on Evaluation of Information Access Technologies, National Center of Sciences, Tokyo, Japan, June 7-10, 2016. National Institute of Informat… [find](https://scholar.google.com/scholar?q=Giovanni+Yoko+Kristianto%2C+Goran+Topic%2C+and+Akiko+Aizawa%2E+2016%2E+MCAT+Math+Retrieval+System+for+NTCIR%2D12+MathIR+Task%2E+In+Proceedings+of+the+12th+NTCIR+Conference+on+Evaluation+of+Information+Access+Tech)
12. Kenton Lee, Ming-Wei Chang, and Kristina Toutanova. 2019. [Latent Retrieval for Weakly Supervised Open Domain Question Answering](https://md.research.elamur.ai/free/en/papers/lee-2019-latent-retrieval-weakly-supervised-open/). In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics, pages 6086–6096, Florence, Italy. Association for Computational Linguistics.
13. Xianming Li and Jing Li. 2023. [AnglE-optimized Text Embeddings](https://md.research.elamur.ai/free/en/papers/li-2023-angle-optimized-text-embeddings/). CoRR, abs/2309.12871.
14. Zhenghao Liu, Chenyan Xiong, Maosong Sun, and Zhiyuan Liu. 2018. Entity-Duet Neural Ranking: Understanding the Role of Knowledge Graph Semantics in Neural Information Retrieval. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages… [find](https://scholar.google.com/scholar?q=Zhenghao+Liu%2C+Chenyan+Xiong%2C+Maosong+Sun%2C+and+Zhiyuan+Liu%2E+2018%2E+Entity%2DDuet+Neural+Ranking%3A+Understanding+the+Role+of+Knowledge+Graph+Semantics+in+Neural+Information+Retrieval%2E+In+Proceedings+of+the+)
15. Yury A. Malkov and Dmitry A. Yashunin. 2020. Efficient and Robust Approximate Nearest Neighbor Search Using Hierarchical Navigable Small World Graphs. IEEE Trans. Pattern Anal. Mach. Intell., 42(4):824–836. [find](https://scholar.google.com/scholar?q=Yury+A%2E+Malkov+and+Dmitry+A%2E+Yashunin%2E+2020%2E+Efficient+and+Robust+Approximate+Nearest+Neighbor+Search+Using+Hierarchical+Navigable+Small+World+Graphs%2E+IEEE+Trans%2E+Pattern+Anal%2E+Mach%2E+Intell%2E%2C+42%284%29%3A82)
16. Behrooz Mansouri, Vít Novotný, Anurag Agarwal, Douglas W. Oard, and Richard Zanibbi. 2022. Overview of ARQMath-3 (2022): Third CLEF Lab on Answer Retrieval for Questions on Math (Working Notes Version). In Conference and Labs of the Evaluation Forum. [find](https://scholar.google.com/scholar?q=Behrooz+Mansouri%2C+V%C3%ADt+Novotn%C3%BD%2C+Anurag+Agarwal%2C+Douglas+W%2E+Oard%2C+and+Richard+Zanibbi%2E+2022%2E+Overview+of+ARQMath%2D3+%282022%29%3A+Third+CLEF+Lab+on+Answer+Retrieval+for+Questions+on+Math+%28Working+Notes+Version)
17. Ryan McDonald, George Brokos, and Ion Androutsopoulos. 2018. Deep Relevance Ranking Using Enhanced Document-Query Interactions. In Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, pages 1849–1860, Brussels, Belgium. Association for Computational Linguistics. [find](https://scholar.google.com/scholar?q=Ryan+McDonald%2C+George+Brokos%2C+and+Ion+Androutsopoulos%2E+2018%2E+Deep+Relevance+Ranking+Using+Enhanced+Document%2DQuery+Interactions%2E+In+Proceedings+of+the+2018+Conference+on+Empirical+Methods+in+Natural+La)
18. Arvind Neelakantan, Tao Xu, Raul Puri, Alec Radford, Jesse Michael Han, Jerry Tworek, Qiming Yuan, Nikolas Tezak, Jong Wook Kim, Chris Hallacy, Johannes Heidecke, Pranav Shyam, Boris Power, Tyna Eloundou Nekoul, Girish Sastry, Gretchen Krueger, David Schnurr, Felipe Petroski Such, Kenny Hsu, Madelei… — [Text and Code Embeddings by Contrastive Pre-Training](https://md.research.elamur.ai/free/en/papers/neelakantan-2022-text-code-embeddings-contrastive-pre/)
19. Yin Ki Ng, Dallas J. Fraser, Besat Kassaie, George Labahn, Mirette S. Marzouk, Frank Wm. Tompa, and Kevin Wang. 2020. Dowsing for Math Answers with Tangent-L. In Working Notes of CLEF 2020 - Conference and Labs of the Evaluation Forum, Thessaloniki, Greece, September 22-25, 2020, volume 2696 of CEUR… [find](https://scholar.google.com/scholar?q=Yin+Ki+Ng%2C+Dallas+J%2E+Fraser%2C+Besat+Kassaie%2C+George+Labahn%2C+Mirette+S%2E+Marzouk%2C+Frank+Wm%2E+Tompa%2C+and+Kevin+Wang%2E+2020%2E+Dowsing+for+Math+Answers+with+Tangent%2DL%2E+In+Working+Notes+of+CLEF+2020+%2D+Conferenc)
20. Yin Ki Ng, Dallas J. Fraser, Besat Kassaie, and Frank Wm. Tompa. 2021. Dowsing for Answers to Math Questions: Ongoing Viability of Traditional MathIR. In Proceedings of the Working Notes of CLEF 2021 - Conference and Labs of the Evaluation Forum, Bucharest, Romania, September 21st -to - 24th, 2021,… [find](https://scholar.google.com/scholar?q=Yin+Ki+Ng%2C+Dallas+J%2E+Fraser%2C+Besat+Kassaie%2C+and+Frank+Wm%2E+Tompa%2E+2021%2E+Dowsing+for+Answers+to+Math+Questions%3A+Ongoing+Viability+of+Traditional+MathIR%2E+In+Proceedings+of+the+Working+Notes+of+CLEF+2021+)
21. Jianmo Ni, Gustavo Hernandez Abrego, Noah Constant, Ji Ma, Keith Hall, Daniel Cer, and Yinfei Yang. 2022a. [Sentence-T5: Scalable Sentence Encoders from Pre-trained Text-to-Text Models](https://md.research.elamur.ai/free/en/papers/ni-2021-sentence-t5-scalable-sentence-encoders/). In Findings of the Association for Computational Linguistics: ACL 2022, pages 1864–1874, Dublin, Ireland. Associati…
22. Jianmo Ni, Chen Qu, Jing Lu, Zhuyun Dai, Gustavo Hernandez Abrego, Ji Ma, Vincent Zhao, Yi Luan, Keith Hall, Ming-Wei Chang, and Yinfei Yang. 2022b. [Large Dual Encoders Are Generalizable Retrievers](https://md.research.elamur.ai/free/en/papers/ni-2021-large-dual-encoders-generalizable-retrievers/). In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pages 9844…
23. Rodrigo Nogueira, Zhiying Jiang, Ronak Pradeep, and Jimmy Lin. 2020. Document Ranking with a Pre-trained Sequence-to-Sequence Model. In Findings of the Association for Computational Linguistics: EMNLP 2020, pages 708–718, Online. Association for Computational Linguistics. [find](https://scholar.google.com/scholar?q=Rodrigo+Nogueira%2C+Zhiying+Jiang%2C+Ronak+Pradeep%2C+and+Jimmy+Lin%2E+2020%2E+Document+Ranking+with+a+Pre%2Dtrained+Sequence%2Dto%2DSequence+Model%2E+In+Findings+of+the+Association+for+Computational+Linguistics%3A+EMNLP)
24. Yifan Qiao, Chenyan Xiong, Zhenghao Liu, and Zhiyuan Liu. 2019. Understanding the Behaviors of BERT in Ranking. CoRR, abs/1904.07531. [find](https://scholar.google.com/scholar?q=Yifan+Qiao%2C+Chenyan+Xiong%2C+Zhenghao+Liu%2C+and+Zhiyuan+Liu%2E+2019%2E+Understanding+the+Behaviors+of+BERT+in+Ranking%2E+CoRR%2C+abs%2F1904%2E07531%2E)
25. Yingqi Qu, Yuchen Ding, Jing Liu, Kai Liu, Ruiyang Ren, Wayne Xin Zhao, Daxiang Dong, Hua Wu, and Haifeng Wang. 2021. [RocketQA: An Optimized Training Approach to Dense Passage Retrieval for Open-Domain Question Answering](https://md.research.elamur.ai/free/en/papers/qu-2021-rocketqa-optimized-training-approach-dense/). In Proceedings of the 2021 Conference of the North American Chapter of the Ass…
26. Stephen Robertson, S. Walker, S. Jones, M. M. Hancock-Beaulieu, and M. Gatford. 1995. [Okapi at TREC-3](https://md.research.elamur.ai/free/en/papers/robertson-1994-okapi-trec-3/). In Overview of the Third Text REtrieval Conference (TREC-3), pages 109–126. Gaithersburg, MD: NIST.
27. Stephen Robertson and Hugo Zaragoza. 2009. The Probabilistic Relevance Framework: BM25 and Beyond. Found. Trends Inf. Retr., 3(4):333–389. [find](https://scholar.google.com/scholar?q=Stephen+Robertson+and+Hugo+Zaragoza%2E+2009%2E+The+Probabilistic+Relevance+Framework%3A+BM25+and+Beyond%2E+Found%2E+Trends+Inf%2E+Retr%2E%2C+3%284%29%3A333%E2%80%93389%2E)
28. Gerard Salton and Christopher Buckley. 1988. Term-weighting approaches in automatic text retrieval. Information Processing & Management, 24(5):513– 523. [find](https://scholar.google.com/scholar?q=Gerard+Salton+and+Christopher+Buckley%2E+1988%2E+Term%2Dweighting+approaches+in+automatic+text+retrieval%2E+Information+Processing+%26+Management%2C+24%285%29%3A513%E2%80%93+523%2E)
29. Hongjin Su, Weijia Shi, Jungo Kasai, Yizhong Wang, Yushi Hu, Mari Ostendorf, Wen-tau Yih, Noah A. Smith, Luke Zettlemoyer, and Tao Yu. 2023. [One Embedder, Any Task: Instruction-Finetuned Text Embeddings](https://md.research.elamur.ai/free/en/papers/su-2022-one-embedder-any-task-instruction/). In Findings of the Association for Computational Linguistics: ACL 2023, pages 1102–1121, Toronto…
30. Laurens van der Maaten and Geoffrey Hinton. 2008. Visualizing Data using t-SNE. Journal of Machine Learning Research, 9(86):2579–2605. [find](https://scholar.google.com/scholar?q=Laurens+van+der+Maaten+and+Geoffrey+Hinton%2E+2008%2E+Visualizing+Data+using+t%2DSNE%2E+Journal+of+Machine+Learning+Research%2C+9%2886%29%3A2579%E2%80%932605%2E)
31. Liang Wang, Nan Yang, Xiaolong Huang, Binxing Jiao, Linjun Yang, Daxin Jiang, Rangan Majumder, and Furu Wei. 2022. [Text Embeddings by Weakly-Supervised Contrastive Pre-training](https://md.research.elamur.ai/free/en/papers/wang-2022-text-embeddings-weakly-supervised-contrastive/). CoRR, abs/2212.03533.
32. Liang Wang, Nan Yang, Xiaolong Huang, Linjun Yang, Rangan Majumder, and Furu Wei. 2024. [Improving Text Embeddings with Large Language Models](https://md.research.elamur.ai/free/en/papers/wang-2024-improving-text-embeddings-large-language/). CoRR, abs/2401.00368.
33. Shitao Xiao, Zheng Liu, Peitian Zhang, and Niklas Muennighof. 2023. [C-Pack: Packaged Resources To Advance General Chinese Embedding](https://md.research.elamur.ai/free/en/papers/xiao-2023-c-pack-packed-resources/). CoRR, abs/2309.07597.
34. Chenyan Xiong, Zhuyun Dai, Jamie Callan, Zhiyuan Liu, and Russell Power. 2017. End-to-End Neural Ad-hoc Ranking with Kernel Pooling. In Proceedings of the 40th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’17, page 55–64, New York, NY, USA. Associati… [find](https://scholar.google.com/scholar?q=Chenyan+Xiong%2C+Zhuyun+Dai%2C+Jamie+Callan%2C+Zhiyuan+Liu%2C+and+Russell+Power%2E+2017%2E+End%2Dto%2DEnd+Neural+Ad%2Dhoc+Ranking+with+Kernel+Pooling%2E+In+Proceedings+of+the+40th+International+ACM+SIGIR+Conference+on+Re)
35. Richard Zanibbi and Dorothea Blostein. 2012. Recognition and retrieval of mathematical expressions. Int. J. Document Anal. Recognit., 15(4):331–357. [find](https://scholar.google.com/scholar?q=Richard+Zanibbi+and+Dorothea+Blostein%2E+2012%2E+Recognition+and+retrieval+of+mathematical+expressions%2E+Int%2E+J%2E+Document+Anal%2E+Recognit%2E%2C+15%284%29%3A331%E2%80%93357%2E)
36. Richard Zanibbi, Kenny Davila, Andrew Kane, and Frank Wm. Tompa. 2016. Multi-Stage Math Formula Search: Using Appearance-Based Similarity Metrics at Scale. In Proceedings of the 39th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’16, page 145–154, New… [find](https://scholar.google.com/scholar?q=Richard+Zanibbi%2C+Kenny+Davila%2C+Andrew+Kane%2C+and+Frank+Wm%2E+Tompa%2E+2016%2E+Multi%2DStage+Math+Formula+Search%3A+Using+Appearance%2DBased+Similarity+Metrics+at+Scale%2E+In+Proceedings+of+the+39th+International+ACM)
37. Wei Zhong, Sheng-Chieh Lin, Jheng-Hong Yang, and Jimmy Lin. 2023. One Blade for One Purpose: Advancing Math Information Retrieval using Hybrid Search. In Proceedings of the 46th International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’23, page 141–151, New York… [find](https://scholar.google.com/scholar?q=Wei+Zhong%2C+Sheng%2DChieh+Lin%2C+Jheng%2DHong+Yang%2C+and+Jimmy+Lin%2E+2023%2E+One+Blade+for+One+Purpose%3A+Advancing+Math+Information+Retrieval+using+Hybrid+Search%2E+In+Proceedings+of+the+46th+International+ACM+SIGI)
38. Wei Zhong, Shaurya Rohatgi, Jian Wu, C. Lee Giles, and Richard Zanibbi. 2020. Accelerating Substructure Similarity Search for Formula Retrieval. In Advances in Information Retrieval: 42nd European Conference on IR Research, ECIR 2020, Lisbon, Portugal, April 14–17, 2020, Proceedings, Part I, page 71… [find](https://scholar.google.com/scholar?q=Wei+Zhong%2C+Shaurya+Rohatgi%2C+Jian+Wu%2C+C%2E+Lee+Giles%2C+and+Richard+Zanibbi%2E+2020%2E+Accelerating+Substructure+Similarity+Search+for+Formula+Retrieval%2E+In+Advances+in+Information+Retrieval%3A+42nd+European+Con)
39. Wei Zhong, Yuqing Xie, and Jimmy Lin. 2022a. Applying Structural and Dense Semantic Matching for the ARQMath Lab 2022, CLEF. In Proceedings of the Working Notes of CLEF 2022 - Conference and Labs of the Evaluation Forum, Bologna, Italy, September 5th - to - 8th, 2022, volume 3180 of CEUR Workshop Pr… [find](https://scholar.google.com/scholar?q=Wei+Zhong%2C+Yuqing+Xie%2C+and+Jimmy+Lin%2E+2022a%2E+Applying+Structural+and+Dense+Semantic+Matching+for+the+ARQMath+Lab+2022%2C+CLEF%2E+In+Proceedings+of+the+Working+Notes+of+CLEF+2022+%2D+Conference+and+Labs+of+t)
40. Wei Zhong, Jheng-Hong Yang, Yuqing Xie, and Jimmy Lin. 2022b. Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval. In Findings of the Association for Computational Linguistics: EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022, pages 1092–110… [find](https://scholar.google.com/scholar?q=Wei+Zhong%2C+Jheng%2DHong+Yang%2C+Yuqing+Xie%2C+and+Jimmy+Lin%2E+2022b%2E+Evaluating+Token%2DLevel+and+Passage%2DLevel+Dense+Retrieval+Models+for+Math+Information+Retrieval%2E+In+Findings+of+the+Association+for+Computa)
41. Wei Zhong and Richard Zanibbi. 2019. Structural Similarity Search for Formulas Using Leaf-Root Paths in Operator Subtrees. In Advances in Information Retrieval - 41st European Conference on IR Research, ECIR 2019, Cologne, Germany, April 14-18, 2019, Proceedings, Part I, volume 11437 of Lecture Note… [find](https://scholar.google.com/scholar?q=Wei+Zhong+and+Richard+Zanibbi%2E+2019%2E+Structural+Similarity+Search+for+Formulas+Using+Leaf%2DRoot+Paths+in+Operator+Subtrees%2E+In+Advances+in+Information+Retrieval+%2D+41st+European+Conference+on+IR+Researc)

*Updated 31 October 2026*