Lean Finder: Semantic Search For Mathlib That Understands User Intents

Introduction

1. User-centered query synthesis: Analyzes and clusters the semantics of public Lean discussions, then fine-tunes text embeddings on synthesized queries that emulate user intents across diverse intent clusters.
2. Diverse input modalities: Supports informalized statements, synthetic user queries, augmented proof states, and formal statements. Model was trained with over 1.4M query-code pairs in total.
3. Preference alignment: Further aligns Lean Finder with mathematicians' preferences via DPO using human and LLM feedback collected from a deployed web service.

Performance

• 81.6% Top-3 preference rate in a user study with real Lean users.
• 30%+ relative improvement (Recall@1) over previous search engines and GPT-4o on informalized statement queries.
• 16%+ relative improvement on proof state queries.
• Compatible with LLM-based theorem provers as a plug-and-play retrieval backbone.

Model Versions

Usage

Citation