:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Gao, Guoxiong, Sun, Zeming, Jiang, Jiedong, Wang, Yutong, Xu, Jingda, Wu, Peihao, Dai, Bryan, Dong, Bin
Format:	Preprint
Published:	2026
Subjects:	Information Retrieval Artificial Intelligence
Online Access:	https://arxiv.org/abs/2605.13137
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Semantic Search Engine for Mathlib4
by: Gao, Guoxiong, et al.
Published: (2024)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

Herald: A Natural Language Annotated Lean 4 Dataset
by: Gao, Guoxiong, et al.
Published: (2024)

Matlas: A Semantic Search Engine for Mathematics
by: Ju, Haocheng, et al.
Published: (2026)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
by: Ji, Junye
Published: (2026)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

LeanExplore: A search engine for Lean 4 declarations
by: Asher, Justin
Published: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Distilling LLM Feedback for Lean Theorem Proving
by: Narozniak, Gaetan, et al.
Published: (2026)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

On-Premise AI for the Newsroom: Evaluating Small Language Models for Investigative Document Search
by: Hagar, Nick, et al.
Published: (2025)

Automated Conjecture Resolution with Formal Verification
by: Ju, Haocheng, et al.
Published: (2026)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Is Grokipedia Right-Leaning? Comparing Political Framing in Wikipedia and Grokipedia on Controversial Topics
by: Eibl, Philipp, et al.
Published: (2026)

Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization
by: Tao, Yicheng, et al.
Published: (2025)

Federated Transfer Learning Based Cooperative Wideband Spectrum Sensing with Model Pruning
by: Jia, Jibin, et al.
Published: (2024)

Collaborative Automatic Modulation Classification via Deep Edge Inference for Hierarchical Cognitive Radio Networks
by: He, Chaowei, et al.
Published: (2024)

LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
by: George, Robert Joseph, et al.
Published: (2025)

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
by: Onda, Naoto, et al.
Published: (2025)

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
by: Xu, Rongge, et al.
Published: (2025)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
by: Tang, Xichen
Published: (2024)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

Applying Embedding-Based Retrieval to Airbnb Search
by: Abdool, Mustafa, et al.
Published: (2026)

SymphonyQG: Towards Symphonious Integration of Quantization and Graph for Approximate Nearest Neighbor Search
by: Gou, Yutong, et al.
Published: (2024)

ProveRAG: Provenance-Driven Vulnerability Analysis with Automated Retrieval-Augmented LLMs
by: Fayyazi, Reza, et al.
Published: (2024)

Repository-level Code Search with Neural Retrieval Methods
by: Gandhi, Siddharth, et al.
Published: (2025)

DeepRetrieval: Hacking Real Search Engines and Retrievers with Large Language Models via Reinforcement Learning
by: Jiang, Pengcheng, et al.
Published: (2025)

Revisiting General Map Search via Generative Point-of-Interest Retrieval
by: Chen, Dong, et al.
Published: (2026)

WebNavigator: Global Web Navigation via Interaction Graph Retrieval
by: Zhang, Xuanwang, et al.
Published: (2026)

Prospects of Retrieval Augmented Generation (RAG) for Academic Library Search and Retrieval
by: Bevara, Ravi, et al.
Published: (2025)

Combining Textual and Structural Information for Premise Selection in Lean
by: Petrovčič, Job, et al.
Published: (2025)

Behavioral Feature Boosting via Substitute Relationships for E-commerce Search
by: Dong, Chaosheng, et al.
Published: (2026)

Lean-STaR: Learning to Interleave Thinking and Proving
by: Lin, Haohan, et al.
Published: (2024)

Semantic Search for Information Retrieval
by: Farivar, Kayla
Published: (2025)

MIRB: Mathematical Information Retrieval Benchmark
by: Ju, Haocheng, et al.
Published: (2025)

PaperRegister: Boosting Flexible-grained Paper Search via Hierarchical Register Indexing
by: Li, Zhuoqun, et al.
Published: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
by: Jiang, Jiedong, et al.
Published: (2025)